LP, the Larch Prover -- Command summary
LP is a command-driven system. Commands can be entered in upper, lower, or
mixed case. They, and some of their
arguments, can be
abbreviated by unambiguous prefixes of their
hyphen-separated components. LP prompts users for any missing arguments that
it requires to execute a command. The syntax of
each command is illustrated and described more fully in the description for
that command.
Commands for creating axioms and facts
- assert <assertion>+; [ ; ]
- Assert axioms
- declare operators <opdec>+[,]
- Declare operators
- declare sorts <sort>+,
- Declare sorts
- declare variables <vardec>+[,]
- Declare variables
- make <fact-status> ( <names> | conjecture )
- Change the activity or immunity of facts or conjecture
Forward inference commands
- apply <names> to <names>
- Apply the named deduction rules to the named facts
- complete
- Run the Knuth-Bendix completion procedure
- critical-pairs <names> with <names>
- Find critical pair equations between each rewrite rule in the first named
set and each in the second
- fix <variable> as <term> in
<names>
- Eliminate one existential quantifier in the named facts, replacing
the quantified variable by a term
- instantiate ( <variable> by <term> )+,
in <names>
- Instantiate variables and/or eliminate universal quantifiers in the named
facts, replacing the free and quantified variables by the terms
- normalize <names>
[ with [ reversed ] <names> ]
- Normalize the named facts using the (reversals of the) hardwired and named
rewrite rules
- rewrite <names>
[ with [ reversed ] <names> ]
- Rewrite some subterm of each named
fact using a hardwired or (the reversal of) a named rewrite rule
Backward inference commands
- apply <names> to conjecture
- Attempt to prove the current conjecture using the named deduction rules
- cancel [ all | lemma ]
- Cancel the current conjecture [and others]
- normalize conjecture [ with <names> ]
- Normalize the current conjecture using all hardwired and named rewrite
rules
- prove <conjecture> [ by <proof-method> ]
- Attempt to prove the conjecture using <proof-method>
- qed
- Check that all conjectures have been proved
- resume [ by <proof-method> ]
- Resume work on the current conjecture using <proof-method>
- rewrite conjecture
[ with [ reversed ] <names> ]
- Rewrite some subterm of the current conjecture
using some hardwired or named rewrite rule
- <>
- Confirm the start of a subgoal in a proof
- []
- Confirm the conclusion of a step in proof
Commands for user interaction
- clear
- Discard all information except global settings
- delete <names>
- Delete the named facts
- define-class $<class> <names>
- Define an abbreviation for <names>
- display [ <information-type> ] [ <names> ]
- Print information about the named facts
- execute <file>
- Execute commands from <file>.lp
- execute-silently <file>
- Same as execute, but suppressing all output
- forget [ pairs ]
- Discard information to save space
- freeze <file>
- Save the state of LP in <file>.lpfrz
- help <topic>
- Print help about the topics
- history [ <number> | all ]
- Print a history of [the <number> most recent] commands
- pop-settings
- Restore the values of local LP settings
- push-settings
- Remember the values of local LP settings
- quit, q
- Exit from LP
- set
- Print the current values of all LP settings
- set <setting-name>
- Print the current value of a setting and prompt for a new value
- set <setting-name> <setting-value>
- Change the value of a setting
- show normal-form <term>
- Display the reduction of a term to normal form
- show unifiers <term>, <term>
- Display all unifiers of two terms
- statistics [ <statistics-option> ]
- Print statistics on runtime, storage, and rule usage
- stop
- Stop execution of command files
- thaw <file>
- Restore a frozen state from <file>.lpfrz
- unset [ <setting> | all ]
- Reset setting to its default value
- version
- Display information about the current version of LP
- write <file> [ <names> ]
- Write the registry and the named facts to <file>.lp
- % <comment>
- Record a comment in the log and/or script file
Commands to control ordering
- order [ <names> ]
- Orient the named formulas into rewrite rules
- register <ordering-constraints>
- Provide constraints for orienting formulas
- unorder [ <names> ]
- Turn the named rewrite rules back into formulas
- unregister <ordering-information>
- Cancel the constraints for orienting formulas