LP, the Larch Prover -- Proofs by contradiction
Proofs by contradiction provide an indirect method of proof. The command
prove F by contradiction directs LP to prove a formula F by deriving
an inconsistency from LP's logical system supplemented
by the hypothesis ~F', where F' is the result of substituting new
constants for the free variables in F. (This hypothesis
is logically equivalent to the negation of F because introducing new
constants is equivalent to replacing the implicit universal quantifiers by
existential quantifiers.) The name of the hypothesis has the form
<simpleId>ContraHyp.<number>, where <simpleId> is the current value
of the name-prefix setting.
The command resume by contradiction directs LP to resume the proof of the
current conjecture by contradiction.