LP, the Larch Prover -- Proofs by consistency
LP permits manual proofs by consistency (also known as proofs by
inductionless induction) in logical systems that consist solely of
quantifier-free equations and rewrite rules. Such proofs require that the
Huet-Hullot principle of definition be satisfied, that is, that all
ground (variable-free) terms be equal, with respect to the equations and
rewrite rules in the system, to ground terms involving a set of free
generators. In axiomatizations of abstract data types, the generators of
the data type will usually have this property. Axiomatizations of sets usually
fail to satisfy the property because the insert operator is not free.
A proof by consistency proceeds by adding an equation to a complete
system and running the completion procedure. If that procedure terminates
without generating an inconsistency, then the equation
is valid in the initial model; if it terminates with an inconsistency, the
equation is not valid; if it does not terminate, the equation may or may not be
valid.