LP, the Larch Prover — The forget command

The forget command causes LP to discard certain information about which computations LP has already performed.

Syntax

<forget-command> ::= forget [ pairs ]

Note: The argument of the forget command can be abbreviated.

Examples

forget

Usage

The forget command causes LP to discard all information about which critical pairs have already been computed in the current proof context. It also prevents LP from accumulating further such information in the current proof context, and in all subsequently created subcontexts, until the next complete command is given.

The forget command can save significant space when there are many rewrite rules. It is useful when we are interested proving conjectures without appealing to the critical-pairs or complete commands.