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
associativecommutative (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 termrewriting
to match and unify terms modulo the
ac and commutative operator theories.
<operatortheory> ::= (ac  commutative) <operator>
Examples
ac +
commutative gcd
Usage
Users can assert or prove operator theories.
LP hardwires the logical connectives /\, \/, and
<=> as associativecommutative 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 operatortheories (or disp ot for short).