LP, the Larch Prover -- Rewrite rules

A rewrite rule is an operational form for a formula. LP uses rewrite rules to rewrite terms to logically equivalent terms.

Syntax

<rewrite-rule> ::= <term> -> <term>

Restrictions: The two <term>s in a rewrite rule must have the same sort. The left side of the rule must not be a variable, the logical constant true, or the logical constant false. Every free variable in the right side must also occur free in left side.

Examples

x + 0 -> x
x <= y -> x < y \/ x = y
x | y -> \E z (y = x*z)
0 < 1 -> true

Usage

Users cannot assert or prove rewrite rules directly. Instead, they must assert or prove formulas, which LP then orients into rewrite rules. The logical content of a term is the equation that results from replacing -> by =.

LP maintains the invariant that all active rewrite rules have been applied to all nonimmune formulas, rewrite rules, and deduction rules in the system.

Some rewrite rules are hardwired into LP to define properties of the logical connectives, the conditional and equality operators, and the quantifiers.

The restriction that the left side of a rewrite rule not be a variable prevents ``rules'' like x -> f(x) from leading to a nonterminating rewriting sequence such as x -> f(x) -> f(f(x)) -> .... The restriction that it not be true or false preserves the meaning of those logical constants. The restriction that the right side not introduce a free variable is more technical. It prevents logically equivalent ``rules'' such as f(x) -> f(y) and f(u) -> f(v) from producing different results when applied to terms like y + f(x).