LP, the Larch Prover -- Brute-force orderings
LP's brute-force ordering procedures give users complete control over the
direction in which formulas are oriented into
rewrite rules, but provide no guarantees about
termination.
The left-to-right ordering
This ordering method causes LP to orient equations into rewrite rules from left
to right, provided the results are valid rewrite rules. Equations that cannot
be oriented from left to right are left unoriented.
The either-way ordering
This ordering method causes LP to orient equations into rewrite rules from left
to right, provided the results are valid rewrite rules. If an equation cannot
be oriented from left to right, but can be from right to left, the method
causes it to be oriented in that direction; otherwise it is left unoriented.
The manual ordering
When the automatic-registry setting is off, this ordering method
causes LP to interact with the user to select an
orientation for each equation. When the setting is on, this ordering
method does not orient any formulas into rewrite rules.