LP, the Larch Prover -- Deduction rules

A deduction rule is logically equivalent to a single formula in multisorted first-order logic. That formula has the form of a logical implication. LP uses deduction rules to derive consequences from other formulas and rewrite rules.

Syntax

<deduction-rule> ::= when <hypothesis>+, yield <conclusion>+,
<hypothesis>     ::= <formula>
<conclusion>     ::= <formula>

Examples

when x < y, y < z yield x < z
when p /\ q yield p, q
when \A e (e \in s1 <=> e \in s2) yield s1 = s2

Usage

Users can assert or prove deduction rules. A deduction rule is logically equivalent to the formula obtained by having the conjunction of its hypotheses imply the conjunction of its conclusions. Thus the first example is logically equivalent to the formula x < y /\ y < z => x < z.

A deduction rule can be applied to a formula or rewrite rule if there is a substitution that matches the first hypothesis of the deduction rule to the formula or rewrite rule. The result of applying a deduction rule with one hypothesis is the set of formulas obtained by applying the substitution(s) that matched its hypothesis to each of its conclusions. For example, applying the second example to 1 < f(x) /\ f(x) < 2 yields two formulas, 1 < f(x) and f(x) < 2. Likewise, applying the third example to x \in s <=> x \in (s \U s) yields the formula s = s \U s.

The result of applying a deduction rule with more than one hypothesis is the set of deduction rules obtained by deleting its first hypothesis (i.e., the one that was matched) and applying the substitution(s) that matched this hypothesis to the remainder of the deduction rule. For example, applying the first example to the formula a < b yields the deduction rule 

when b < z yield a < z
On the other hand, applying the logically equivalent deduction rule 
when y < z, x < y yield x < z
to the same formula yields a different result, namely, 
when x < a yield x < b

When applying deduction rules, LP produces the strongest valid conclusions by changing, when appropriate, variables in the conclusions that do not occur freely in the hypotheses. For example, applying the deduction rule 

when P(x) yield Q(x, y)
to the formula P(f(y)) yields the result Q(f(y), y1) and not the weaker result Q(f(y), y).

The results of applying a deduction rule are given the default activity and immunity, as established by the set command.

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

To display the deduction rules that LP currently has available for use, type display deduction-rules (or disp d-r for short).

See formulas for a list of deduction rules that are hardwired into LP. See also partitioned-by.