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.