LP, the Larch Prover -- The ordering-method setting
The ordering-method setting specifies the method used to orient formulas
into rewrite rules.
Note: The <ordering> can be abbreviated.
<set-ordering-method-command> ::= set ordering-method <ordering>
<ordering> ::= <registered-ordering>
| either-way | left-to-right
| manual | polynomial [ <number> ]
<registered-ordering> ::= dsmpos | noeq-dsmpos
set ordering dsmpos
set ordering polynomial 2
The set ordering-method command sets the method used to orient formulas
into rewrite rules in the current proof context. The methods based on the
polynomial orderings attempt to guarantee that
the resulting set of rewrite rules is terminating. The other
brute-force orderings give users more control
over the direction in which equations are oriented into rewrite rules, but they
do not guarantee termination. The registered orderings are the easiest to use.
The default ordering method is noeq-dsmpos.
When a set of rewrite rules is known to terminate (because of the ordering used
to orient them), but the new ordering does not establish termination, LP issues
a warning that the termination proof will be lost when the next rewrite rule is
added to the system.