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