ded abstract of this paper is published in the proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems, Pont- -Mousson, 1992 1
A new positive-unit theorem-proving procedure for equational Horn clauses is presented. It uses a term ordering to restrict paxamodulation to potentiallymaximal sides of equations...
We show that a simple, and easily implementable, restriction on the recursive path ordering, which we call the "binary path condition," sufficesfor establishing terminat...