ProofCommands.txt revision 17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19
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
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till 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
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | show theory -- show current theory and proof goals
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | translate COMORPHISM -- translate theory goals along comorphism
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | start PROVER -- start a prover
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | <prover-specific commands> -- e.g. Isabelle, SPASS
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiDG-COMMAND ::= auto -- automatic tactic
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | globSubsume -- global subsumption
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | globDecomp -- global decomposition
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | locInfer -- local inference
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | locDecomp -- local decomposition
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | comp -- composition
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | compNew -- composition with speculation of new egdes
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | hideThm -- Hide-Theorem-Shift
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | thmHide -- Theorem-Hide-Shift
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski | basicInfer -- prove at a particular node,
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till Mossakowski -- i.e. start local proving in a theory
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiGOAL ::= DIGIT* -- specify goals by their number
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiCOMORPHISM ::= ID ; ... ; ID -- composite of basic comorphisms
17cd531da84dd53bbe5bcd1f513e9ff93c9d1c19Till MossakowskiPROVER ::= ID -- name of prover