ProofCommands.txt revision 52791eb67eec531963ee9c0e4b79770c3d15e15b
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
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- if no goal is specified, all goals are tried
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | show -- display list of open dg goals
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- commands for theory mode
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | show -- display list of theory goals
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski | show-theory -- show current theory and proof goals
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
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski | prove FORMULA*
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski | prove FORMULA* axioms FORMULA+
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- insert initial proof script
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- insert only the specified formulas as goals (top goal if none is specified)
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski -- insert only the specified axioms
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski | prove-all FORMULA*
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski | prove-all FORMULA* axioms FORMULA+
52791eb67eec531963ee9c0e4b79770c3d15e15bTill Mossakowski -- same for all goals
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill MossakowskiPROOF-SCRIPT -- can be anything (prover specific)
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski -- the end is recognized with "end-script"
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till 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
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till 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
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski | basic -- prove 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
b32e84ad2e22057345d18361ffa2d78772e69e50Till MossakowskiNODE ::= ID -- specify nodes with their names
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiCOMORPHISM ::= ID ; ... ; ID -- composite of basic comorphisms
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill MossakowskiPROVER ::= ID -- name of prover
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill MossakowskiFORMULA ::= ID -- label of formula