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.