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.

Syntax

<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