LP, the Larch Prover -- The hardwired-usage setting
The hardwired-usage setting provides users with limited control over LP's
use of hardwired rewrite and deduction rules.
<set-hardwired-usage-command> ::= set hardwired-usage <number>
Examples
set hardwired-usage 8
Usage
LP hardwires selected rewrite rules for the logical and
conditional operators. For debugging purposes, the
set hardwired-usage command can be used to turn off some of these
hardwired rewrite rules in the current proof context. The following powers of
2, if they occur in the binary representation of
<number>, turn off the indicated rule.
- 2
- Turns off the rewrite rule x => false -> ~x
- 4
- Turns off the rewrite rule x <=> false -> ~x, but adds the rewrite
rule x <=> y <=> ~y -> ~x.
- 8
- Turns off the rewrite rules with left side if x then y else z when
y or z is true or false
- 16
- Turns off the if-simplification metarule