LP, the Larch Prover -- The ordering-method setting

The ordering-method setting specifies the method used to orient formulas into rewrite rules.

Syntax

<set-ordering-method-command> ::= set ordering-method <ordering>
<ordering>                    ::= <registered-ordering> 
                                     | either-way | left-to-right 
                                     | manual | polynomial [ <number> ]
<registered-ordering>         ::= dsmpos | noeq-dsmpos

Note: The <ordering> can be abbreviated.

Examples

set ordering dsmpos
set ordering polynomial 2

Usage

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 registered and 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.