Language for the Hets command line interface

SCRIPT ::= COMMAND*

COMMAND ::=

-- commands for development graph mode

use PATH -- open a file with a HetCASL library

-- this will compute a development graph

-- and a list of open proof obligations

-- also all referenced libraries need to be loaded

-- (and this needs to be communicated to PGIP)

| dg DG-COMMAND GOAL* -- apply a proof step of the dg calculus

-- if no goal is specified, the first goals is tried

| dg-all DG-COMMAN -- same, but for all open goals

| show-dg-goals -- display list of open dg goals

-- commands for theory mode

| show-theory-goals -- display list of theory goals

| show-theory -- show current theory and proof goals

| node-info -- show info about current dg node (name, origin, sublogic)

| show-taxonomy -- show taxonomy graph

| show-concepts -- show conecpt graph

| translate COMORPHISM -- translate theory goals along comorphism

| prover PROVER -- select a prover

| proof-script FORMULA PROOF-SCRIPT end-script

-- process proof script for one goal

| cons-check PROVER -- check consistency

-- interactive commands for theory mode

| prove FORMULA* AXIOM-SELECTION?

-- insert initial proof script

-- insert only the specified formulas as goals (top goal if none is specified)

-- insert only the specified axioms (otherwise, insert all axioms)

| prove-all AXIOM-SELECTION?

-- same for all goals

AXIOM-SELECTION ::=

with FORMULA+ -- include only specified axioms

| exlcuding FORMULA+ -- exlcude specified axioms

PROOF-SCRIPT -- can be anything (prover specific)

-- the end is recognized with "end-script"

DG-COMMAND ::= auto -- automatic tactic

| glob-subsume -- global subsumption

| glob-decomp -- global decomposition

| loc-infer -- local inference

| loc-decomp -- local decomposition

| comp -- composition

| comp-new -- composition with speculation of new egdes

| hide-thm -- Hide-Theorem-Shift

| thm-hide -- Theorem-Hide-Shift

| basic -- start proving at a particular node,

-- i.e. start local proving in a theory

GOAL ::= NODE -- select local goals at a node

| NODE -> NODE -- select all edges between two given nodes

| NODE - DIGIT* -> NODE -- select specific edge between two nodes

NODE ::= ID -- specify nodes with their names

COMORPHISM ::= ID ; ... ; ID -- composite of basic comorphisms

-- if jsut one logic name is given, the default is used

PROVER ::= ID -- name of prover

FORMULA ::= ID -- label of formula

PATH ::= -- path name (look at CASL syntax)

ID ::= -- identifier (look at CASL syntax)