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: 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.

Syntax

<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).