1
$\begingroup$

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical one in the overall attempt to get to the point where equations can be applied in one direction, thereby dramatically improving the performance of automated reasoning on problems involving equality.)

If $s \succ t \succ u$

Let $s\approx t$ have the multiset representation $\{\{s\},\{t\}\}$

Let $s\not\approx t$ have the multiset representation $\{\{s,\bot\},\{t,\bot\}\}$ where $\bot$ is a new symbol such that every existing symbol is greater than $\bot$.

Then $s\not\approx u \succ s\approx t$ even though $t \succ u$.

... wait, how? Sure, $s\not\approx u$ also contains a couple of occurrences of $\bot$, but what of that? $t \succ u \succ \bot$, so the comparison should be decided by $t$ vs. $u$; $\bot$ should not have enough weight to tip the balance, so to speak.

What am I missing?

(I have seen later writing that gives $s\not\approx t$ the multiset representation $\{\{s,s\},\{t,t\}\}$, and I see how this solves the problem, but I don't see how it is solved in the original version.)

$\endgroup$
  • 1
    $\begingroup$ Technically the $\{\{s\},\{t\}\}$ representation is a multiset of multisets representation. Might be worth noting to avoid any confusion. $\endgroup$ – Dmitri Chubarov Jan 13 at 7:58
1
$\begingroup$

A short answer to your question is to use the definition of multiset extension of a partial ordering.

We have the following:

  1. Let $M = \{s,\bot\}$ and $N=\{s\}$. We have $M\succ M$ since $M(\bot) > N(\bot)$ and there does not exist $x$ such that $N(x)> M(x)$.
  2. Let $M=\{\{s,\bot\},\{u,\bot\}\}$ and $N=\{\{s\},\{t\}\}$. We have $M(\{s,\bot\})>N(\{s,\bot\})$ and by (1) $\{s,\bot\}\succ\{s\}$. Therefore $M\succ N$.

It would be interesting to see examples where the two ways of extending an ordering on equations to clauses disagree and discuss how that might affect the properties or performance of a rewrite-based prover.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.