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.

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.

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