LP, the Larch Prover -- The dsmpos ordering

The dsmpos ordering is a registered ordering used to orient formulas into rewrite rules. It defines a well founded partial order on terms from a partial order on operators, given by height constraints, and from status constraints. When no associative-commutative operators or quantifiers are present, the rewrite relation of the set of rewrite rules produced by the dsmpos ordering is embedded in this well founded partial order on terms and hence is guaranteed to terminate.

The dsmpos ordering computes complete sets of minimal extensions to LP's registry when necessary to orient a formula. The noeq-dsmpos is the same ordering, except that it does not suggest assigning equal heights to two operators; as a result, it is faster, but less powerful than dsmpos.

Let s and t be two terms, with s = f(s1, ..., sm) and t = g(t1, ..., tn). Then s >= t in the dsmpos ordering iff

si >= t for some i, or
f > g (i.e., f is higher than g in the registry) and s > ti for all i, or
either f and g have the same height in the registry, or f >= g and s > ti for all i, and in either case
- if both f and g can have multiset status, then the multiset {s1, ..., sm} is greater than or equal to the multiset {t1, ..., tn}, or
- if both f and g can have lexicographic status, then s > ti for all i and the sequence < s1, ..., sm > is lexicographically greater than or equal to the sequence < t1, ..., tn >.

Here M1 is greater than or equal to M2 as a multiset iff M2 has the same elements, though possibly with different multiplicities, as (M1 - X) U Y, where X and Y are multisets such that for any y in Y there is an x in X with x > y.

The dsmpos ordering is based on the recursive path ordering with status due to Dershowitz, Kamin, and Levy. The definition of the ordering >= is due to Forgaard. The generation of suggestions is due to Detlefs and Forgaard.

LP uses the following modification of the dsmpos ordering to orient equations that contain quantifiers. It replaces each quantifier (over a sort S) in an equation by a pseudo-operator with signature S, Bool -> Bool, and it replaces each bound variable by the constant true; in this way, it converts each subterm of the form \E x P(x) or \A x P(x) in an equation into a subterm \E(true, P(true)) or \A(true, P(true)). (In general, the resulting term does not sort check.) Then LP tries to orient the transformed equation with the aid of registry suggestions for the pseudo-operators. It it succeeds, it orients the original equation in the same direction as its transformation.