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.

Syntax

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