# Ordering of multisets in “Paramodulation based theorem proving”

and I can't understand a part of it. it defines an ordering on multisets (it defines a multiset over $A$ as a function $A \rightarrow N$)

and says (page 13) multisets are ordered by the smallest irreflexive, transitive relation $\succ\succ$ such that $M \cup \{s\} \succ\succ N \cup \{t_1,\ldots,t_n\} \; \mbox{if} \; M==N \land s \succ t_i \; \forall i \in 1 \ldots n$

but later it says (page 24) $\{s, t\} \succ\succ \{u, v\}$ if $\\s > u \land (s \geq v \lor t \geq v) \;\lor\; s > v \land (s \geq u \lor t \geq u) \;\lor\\ t > u \land (s \geq v \lor t \geq v) \;\lor\; t > v \land (s \geq u \lor t \geq u)$

(by page 15, $>$ and $=$ are interpreted as a given total (up to $=_c$)reduction ordering $\succ$ and congruence $=_c$ respectively)

which would seem to make $\succ\succ$ not aymmetric, but it must be asymmetric as it is transitive and irreflexive

the problem is that it could be the case that $s > u \land s = v$ which would make $\{s, t\}$ greater but also $v > t \land s = v$ which would make $\{u, v\}$ greater if we apply the rule backwards

I guess it might be the case that this rule only works because of constraints on the multisets

The way the E theorem prover computes this seems to make sense:

  int LiteralCompareFun(Eqn_p lit1, Eqn_p lit2)
{
int cmpres;

if(EqnIsPositive(lit1) && !EqnIsPositive(lit2))
{
return 1;
}
else if(!EqnIsPositive(lit1) && EqnIsPositive(lit2))
{
return -1;
}
cmpres = PCmp(MAX(lit1->lterm, lit1->rterm),
MAX(lit2->lterm, lit2->rterm));

if(cmpres)
{
return cmpres;
}
return PCmp(MIN(lit1->lterm, lit1->rterm),
MIN(lit2->lterm, lit2->rterm));
}

-
You’ve inverted every order from p. 13, and you’ve transcribed the constraints on p. 24 incorrectly: they involve the binary predicate symbol $>$, defined on p. 15, which is not the same as $\succ$. – Brian M. Scott Jul 11 '12 at 9:10
I think I fixed the problems – Emma Jul 11 '12 at 9:30