LP, the Larch Prover — The automatic-ordering setting


The automatic-ordering setting controls whether LP orients formulas into rewrite rules with or without the user having to issue an explicit order command.

Syntax

<set-automatic-ordering-command> ::= set automatic-ordering ( on | off )

Examples

set auto-ord off

Usage

If automatic-ordering is on (the default), then LP attempts to orient all formulas (asserted axioms, proved conjectures, results of deductions, instantiations, critical pair equations, and hypotheses for subgoals in proofs) automatically into rewrite rules. If it is off, then the user must issue an explicit order command to orient formulas into rewrite rules. The value of this setting is local to the current proof context.