LP, the Larch Prover -- The register command

The register command provides LP with hints for use in orienting formulas into terminating sets of rewrite rules.

Syntax

<register-command>    ::= register <ordering-constraint>
<ordering-constraint> ::= <height-constraint> | <status-constraint>
                             | <polynomial-constraint>

Note: The first word in the <ordering-constraint> can be abbreviated.

Examples

register height f > g
register status multiset +
register polynomials + x + y + 1, x + 2

Usage

The register command adds constraints to a registry that LP uses in conjunction with ordering methods that attempt to orient formulas into a set of terminating rewrite rules. The height and status constraints are used by LP's registered orderings, and the polynomial constraints are used by LP's polynomial ordering.

When the automatic-registry setting is on and the ordering-method setting is a registered ordering, LP automatically adds height and status constraints to the registry, as necessary, to orient equations in order to ensure that the resulting set of rewrite rules is terminating.

The display ordering command displays the constraints in the registry. Ordering constraints can be removed from the registry with the unregister command.