1
$\begingroup$

Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, u>v (after substitution, and assuming the terms can be ordered). Equivalently, !(u<=v), after substitution.

However, Schulz 2006, 'Algorithms and Data Structures for First-Order Equational Deduction', specifies the criterion as u>=v (after substitution, and assuming the terms can be ordered). Equivalently, !(u<v), after substitution.

As far as I can tell so far, the latter is correct. For example, TPTP problem SET836-2 seems to be only solvable by allowing applications of superposition that generate clauses ... | true!=true (where true!=true then of course disappears, but disallowing it seems to break completeness for that problem). So it seems it is actually necessary to allow the two terms to be equal.

Is this a case of the older paper simply containing an error which was later discovered? Or am I misinterpreting it, or are they correct given some other condition?

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.