Multiset Ordering

The multiset ordering over the set S is the transitive closure of a relation P on the collection of finite multisets over S. If R is a partial ordering on S then aPb if and only if for some x∈D(b):

So, if we have a multiset b and we replace some element x∈D(b) with occurrences of elements x0,...,xn such that 0≤i≤n xiRx to give the multiset a, then aPb.

The multiset ordering over a well-founded ordering is well-founded.


Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.