LP, the Larch Prover -- The activity setting
LP automatically uses all active rewrite rules for normalization and all
active deduction rules for deduction. By contrast, it uses passive facts
only upon explicit user command. The activity of newly asserted or conjectured
facts is governed by the activity setting. The activity of previously
asserted or conjectured facts can be changed by the make command.
Unless instructed otherwise, LP treats all facts as active.
<set-activity-command> ::= set activity ( on | off )
Examples
set activity off
Usage
The activity 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 active if the setting is on (the default) and
passive (or inactive) if it is off. Passive facts are
indicated by a parenthesized letter (P) in the output of the
display command.
LP automatically uses all active rewrite rules to reduce
terms to normal form, and it automatically uses all
active deduction rules to deduce consequences from
formulas and rewrite rules. LP does not make automatic use of passive facts.
Instead, LP applies passive rewrite rules only in response to the
normalize or rewrite commands, and it applies passive
deduction rules only in response to the apply command.
Facts retain their activity or passivity when they are normalized, and formulas
retain their activity or passivity when oriented into rewrite rules. Likewise,
passive conjectures remain passive when proved.
There are two main uses for passive facts in LP.
-
Users can improve the performance of LP by declaring facts to be passive when
they are known to be inapplicable. When LP subsequently adds new formulas to
the system, it will not attempt to reduce them by passive rules or to apply
passive deduction rules to them.
-
Users can control the application of problematic rewrite and deduction rules by
declaring them to be passive. For example, users may wish to apply a complete
set of boolean reductions when they believe it will simplify a formula (e.g.,
to true), but they may be reluctant to have LP apply those reductions
automatically to all formulas (lest the reductions produce large, unreadable
intermediate forms).