LP, the Larch Prover -- The order command

The order command directs LP to attempt to orient formulas into rewrite rules.

Syntax

<order-command> ::= order [ <names> ]

Examples

order
order nat

Usage

When the automatic-ordering setting is on, LP attempts to orient formulas into rewrite rules automatically. When it is off, LP orients formulas only in response to an explicit order or complete command. If no <names> are specified in an order command, LP attempts to orient all formulas in the system. If <names> are specified, LP attempts to orient only the named formulas (including any new formulas that LP generates during the ordering process, for example, as a result of applying a deduction rule to a newly reduced fact).

When a formula is an equation t1 = t2 or t1 <=> t2, LP uses the current ordering-method, if possible, to orient it into the rewrite rule t1 -> t2 or into the rewrite rule t2 -> t1. When a formula f is not an equation (i.e., when its principal operator is neither = nor <=>), LP orients it into the rewrite rule f -> true (or into the rewrite rule f1 -> false, if f has the form ~f1).

If the current ordering method is a registered or polynomial ordering, the order command also attempts to orient the formulas into a provably terminating set of rewrite rules. If the current ordering method is a brute-force ordering, the order command may orient the formulas into a nonterminating set of rewrite rules.

Users can interrupt and resume the operation of the order command.