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.