17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiLanguage for the Hets command line interface
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiSCRIPT ::= COMMAND*
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- commands for development graph mode
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski use PATH -- open a file with a HetCASL library
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- this will compute a development graph
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- and a list of open proof obligations
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- also all referenced libraries need to be loaded
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- (and this needs to be communicated to PGIP)
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski | dg DG-COMMAND GOAL* -- apply a proof step of the dg calculus
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski -- if no goal is specified, the first goals is tried
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | dg-all DG-COMMAN -- same, but for all open goals
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | show-dg-goals -- display list of open dg goals
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- commands for theory mode
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | show-theory-goals -- display list of theory goals
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski | show-theory -- show current theory and proof goals
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | node-info -- show info about current dg node (name, origin, sublogic)
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | show-taxonomy -- show taxonomy graph
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | show-concepts -- show conecpt graph
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | translate COMORPHISM -- translate theory goals along comorphism
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski | prover PROVER -- select a prover
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski | proof-script FORMULA PROOF-SCRIPT end-script
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- process proof script for one goal
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | cons-check PROVER -- check consistency
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski -- interactive commands for theory mode
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | prove FORMULA* AXIOM-SELECTION?
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- insert initial proof script
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- insert only the specified formulas as goals (top goal if none is specified)
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski -- insert only the specified axioms (otherwise, insert all axioms)
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | prove-all AXIOM-SELECTION?
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- same for all goals
1d49bdc3171a64621bc8e710c9f155a929425f61Till MossakowskiAXIOM-SELECTION ::=
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski with FORMULA+ -- include only specified axioms
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | exlcuding FORMULA+ -- exlcude specified axioms
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill MossakowskiPROOF-SCRIPT -- can be anything (prover specific)
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski -- the end is recognized with "end-script"
1d49bdc3171a64621bc8e710c9f155a929425f61Till MossakowskiDG-COMMAND ::= auto -- automatic tactic
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | glob-subsume -- global subsumption
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | glob-decomp -- global decomposition
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | loc-infer -- local inference
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | loc-decomp -- local decomposition
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | comp -- composition
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | comp-new -- composition with speculation of new egdes
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | hide-thm -- Hide-Theorem-Shift
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | thm-hide -- Theorem-Hide-Shift
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski | basic -- start proving at a particular node,
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski -- i.e. start local proving in a theory
b32e84ad2e22057345d18361ffa2d78772e69e50Till MossakowskiGOAL ::= NODE -- select local goals at a node
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | NODE -> NODE -- select all edges between two given nodes
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | NODE - DIGIT* -> NODE -- select specific edge between two nodes
1d49bdc3171a64621bc8e710c9f155a929425f61Till MossakowskiNODE ::= ID -- specify nodes with their names
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiCOMORPHISM ::= ID ; ... ; ID -- composite of basic comorphisms
1d49bdc3171a64621bc8e710c9f155a929425f61Till Mossakowski -- if jsut one logic name is given, the default is used
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill MossakowskiPROVER ::= ID -- name of prover
1d49bdc3171a64621bc8e710c9f155a929425f61Till MossakowskiFORMULA ::= ID -- label of formula
1d49bdc3171a64621bc8e710c9f155a929425f61Till MossakowskiPATH ::= -- path name (look at CASL syntax)
1d49bdc3171a64621bc8e710c9f155a929425f61Till MossakowskiID ::= -- identifier (look at CASL syntax)