LP, the Larch Prover — Proofs by normalization

LP uses active rewrite rules to normalize conjectures. If a conjecture normalizes to true, it is a theorem. Otherwise, the normalized conjecture becomes the current subgoal to be proved. For example, LP succeeds in proving the conjecture

{e} \subseteq insert(e, s)

from the axioms

{e} = insert(e, {})
e \in insert(e1, x) <=> e = e1 \/ e \in s
{} \subseteq s
insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y

by using them to reduce it to true. But the conjecture x \subseteq x is irreducible, and LP treats it as a subgoal to be proved by some other proof method.

Passive rewrite rules can be applied explicitly to a conjecture by the normalize and rewrite commands. These commands can be used to control when definitions are expanded, or when nonsimplifying rewrite rules (such as distributivity) are applied.