LP, the Larch Prover -- Equality operators


LP automatically declares an equality operator = and an inequality operator ~= with signature S,S:->Bool for each sort S. These operators have the standard interpretation: two objects of some sort S are equal if and only if they are identical.

Operationally, LP uses equational term-rewriting to reduce a term t to a normal form t' such that the formula t = t' is true. For this purpose, LP: