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:
-
treats the equality operator as commutative except
when S is Bool, in which case LP treats it as a synonym for the
associative-commutative operator <=> for
logical equivalence.
-
uses two hardwired rewrite rules for each sort S
- x:S = x:S -> true
- x:S ~= y:S -> ~(x = y)
-
registers the operators = and ~= as
having multiset status for the purpose of
orienting formulas into rewrite rules.