Question

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.)

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top