ProofCommands.txt revision c94305f95f2a70ba544d40c7dd1cbd6c54e2d3dd
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
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
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski | proof-script PROVER PROOF-SCRIPT end-script
b32e84ad2e22057345d18361ffa2d78772e69e50Till Mossakowski -- process proof script, e.g. Isabelle, SPASS,...
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski | prover PROVER FORMULA*
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski | prover PROVER FORMULA* axioms FORMULA+
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski -- start a prover, with Hets inserting initial proof script
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski -- insert only the specified formulas as goals (all if none is specified)
c94305f95f2a70ba544d40c7dd1cbd6c54e2d3ddTill Mossakowski -- insert only the specified axioms
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