LP, the Larch Prover -- The forget command
The forget command causes LP to discard certain information about which
computations LP has already performed.
<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.