LP, the Larch Prover — Proof methods for formulas

LP provides a variety of methods for proving formulas. Some represent standard proof techniques (proofs by cases, contradiction, induction, and normalization). Two (generalization and specialization) help establish conjectures containing quantifiers. Others assist in proving formulas with particular syntactic forms (implications, logical equivalences, conditionals, and conjunctions).

Syntax

<proof-method>          ::= <default-proof-method> | cases <term>+,
                               | contradiction | default
                               | generalizing <variable> from <term>
                               | induction [ [ on <variable> ]
                                   [ depth <number> ] [ [ using ] <names> ]
                               | specializing ( <variable> to <term> ) +,
<default-proof-method>  ::= /\-method | =>-method | <=>-method | if-method
                               | explicit-commands | normalization

Note: The first word of the <proof-method> can be abbreviated.

Examples

=>
cases x < 0, x = 0, x > 0
induction on x

Usage

Users can specify a method of proof in the prove command that introduces a conjecture, in a subsequent resume command, or in a list of default proof-methods that LP uses when no method is specified in a prove command or when it creates subgoals.

The default method specifies the use of the first applicable proof method in the value of the proof-methods setting. See the individual descriptions of the other proof methods for information about their use.