# 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.
`<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.