LP, the Larch Prover -- Sample proofs: two easy theorems

The proof of the first theorem in set1.lp is straightforward.

set name setTheorems
prove e \in {e}
qed

The prove command directs LP to initiate the proof of a conjecture, and the qed command directs LP to confirm that its proof is complete. LP proves this conjecture automatically by using the user-supplied axioms as rewrite rules. When using a formula as a rewrite rule, either LP rewrites terms matching the entire formula to true or, when the principal connective of the formula is = (equals) or <=> (if and only if), LP rewrites terms matching the left side of the formula to terms matching the right. Occasionally LP will reverse the order of terms in an equality to ensure that the resulting set of rewrite rules does not produce nonterminating (i.e., infinite) rewriting sequences. Here's how LP proves the first conjecture:

e \in {e} ~> e \in insert(e, {})    by setAxioms.2
          ~> e = e \/ e \in {}      by setAxioms.4
          ~> true \/ e \in {}       by a hardwired axiom for =
          ~> true                   by a hardwired axiom for \/

Most proofs require user guidance. For example, to prove that for any two elements e1 and e2, there is a set that contains exactly these two elements, the user must provide a ``witness'' for the existential quantifier in the second conjecture:

prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
  resume by specializing x to insert(e2, {e1})
qed

Users can specify a proof method for a conjecture either as part of the prove command or in a separate resume command, which continues the proof of the conjecture.