LP, the Larch Prover -- Operator theories
An operator theory is logically equivalent to a set of equations
involving a single operator. At present, LP supports two
operator theories:
-
the commutative theory, which is axiomatized by the commutative law
x + y = y + x
-
the
associative-commutative (ac) theory, which is axiomatized by the
commutative law together with the associative law
x + (y + z) = (x + y) + z.
LP uses operator theories to circumvent problems with nonterminating rewriting
systems. Because the commutative law cannot be oriented into a terminating
rewrite rule, LP uses equational term-rewriting
to match and unify terms modulo the
ac and commutative operator theories.
<operator-theory> ::= (ac | commutative) <operator>
Examples
ac +
commutative gcd
Usage
Users can assert or prove operator theories.
LP hardwires the logical connectives /\, \/, and
<=> as associative-commutative operators. It hardwires the
equality operator =:S,S->Bool as a commutative operator
when the sort S is not Bool.
The fact ac op normalizes the fact commutative op to true.
To display the operator theories in LP's logical system, type
display operator-theories (or disp o-t for short).