# 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).
`<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.