LP, the Larch Prover -- The proof-methods setting
The proof-methods setting provides a list of default proof methods for LP
to use when attempting to prove a formula.
Note: Each <default-proof-method> can be abbreviated.
<set-proof-methods-command> ::= set proof-methods <default-proof-method>+[,]
set proof =>, normalization
The set proof-methods command provides a list of default proof methods for
the current proof context. LP uses the first method in the list that applies
to the conjecture. The default list is normalization. Any method (other
than contradiction) that does not mention a variable or constant can
appear on the list. If the proof-method list is explicit-commands, then
LP will await a resume command before beginning the proof.