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