LP, the Larch Prover -- Registered orderings

LP provides two registered orderings, the dsmpos and noeq-dsmpos orderings, which are based on LP-suggested partial orderings of operators and which guarantee termination of the set of rewrite rules when no associative-commutative operators are present. Most users rely on these orderings to orient all formulas. In striking contrast to the brute-force orderings, they hardly ever cause difficulties by producing a nonterminating set of rewrite rules.

Registered orderings use information in a registry to orient formulas into rewrite rules. There are two kinds of information in a registry: height information and status information.

When the current registry does not contain enough information to orient a formula, LP will generate minimal sets of extensions to the registry, called suggestions, that permit the formula to be oriented. If the automatic-registry setting is on, LP picks one of these extensions to orient a formula without user interaction; it does not try all extensions. If the setting is off, LP will interact with the user, who must pick the desired extension.