LP, the Larch Prover — The immunity setting

LP automatically subjects all nonimmunized facts in its logical system to normalization and deduction. By contrast, it subjects immune facts to these operations only upon explicit user command. The immunity of newly asserted or conjectured facts is governed by the immunity setting. The immunity of previously asserted or conjectured facts can be changed by the make command. Unless instructed otherwise, LP does not treat any fact as immune.

Syntax

<set-immunity-command> ::= set immunity ( on | off | ancestor )

Note: The immunity setting can be abbreviated.

Examples

set immunity on

Usage

The immunity setting applies to facts and conjectures created by the apply, assert, critical-pairs, fix, instantiate, and prove commands in the current proof context. Such facts are immune if the setting is on, nonimmune if it is off, and ancestor-immune if it is ancestor. Immune facts are indicated by a parenthesized letter (I) in the output of the display command; ancestor-immune facts are indicated by (i).

LP automatically reduces all terms in nonimmune formulas, rewrite rules, and deduction rules to normal form, and it automatically applies all active deduction rules to all nonimmune formulas and rewrite rules. LP behaves differently, however, with respect to immune and ancestor-immune facts.

LP does not automatically reduce immune facts to normal form, and it does not automatically apply deduction rules to them. Instead, LP reduces them only in response to the normalize or rewrite commands, and it uses them for deduction only in response to the apply command.
LP does not automatically reduce an ancestor-immune fact by any ancestor of that fact, and it does not automatically apply a deduction rule that is an ancestor of a fact to that fact. One fact is an ancestor of another if its name is a prefix of the other's. Thus, if rewrite rule a.1.2.3 is ancestor-immune, it will not be reduced by rewrite rule a.1.2 (from which it may have been obtained by instantiation), and it will not have deduction rule a.1 (from which a.1.2 may have been obtained by instantiation) applied to it.

Facts retain their immunity when they are normalized, and formulas retain their immunity when oriented into rewrite rules. Likewise, immune conjectures may be reduced during an attempt to prove them, but are added to the system as immune facts in their original form when proved.

There are several reasons to make facts immune or ancestor-immune in LP.

Immune facts retain their original form and may be more readable than reduced versions of those facts.
Immune rewrite rules may be useful in critical-pair computations.
Setting immunity on or to ancestor makes it possible to preserve instantiations that might otherwise normalize to identities.
Users can improve the performance of LP by declaring facts to be immune when they are known to be irreducible. When LP subsequently adds new rewrite rules to the system, it will not attempt to reduce the immune facts using these rules.

However, there are also disadvantages to making too many rules immune.

The presence of immune rules can degrade the performance of LP, because additional rewrite rules increase the cost of normalization. It can also increase the amount of nonconfluence in a rewriting system.
An immune deduction rule with a reducible hypothesis may not match formulas as expected, because the deduction rule is applied only after the formulas have been normalized.