Solving Term Inequalities

This work pertains to the Knuth-Bendix (KB) algorithm which tries to find a complete set of reductions from a given set of equations. In the KB algorithm a term ordering is employed and it is required that every equation be orientable in the sense that the left-hand side be greater than the right. The KB algorithm halts if a nonorientable equation is produced. A generalization of the KB algorithm has recently been developed in which every equation is orientable and which halts only when a complete set is generated. In the generalization a constraint is added to each equation. The constraint governs when the equation can be used as a reduction. The constraintis obtainedfrom the equationby "solving" the term inequality left-hand side > right-hand side. To understand what it means to solve a term inequality, consider the analogy with algebra in which solving term equalities, i.e. unijicafion, is analogous to solving algebraic equalities. Then solving term inequalities is ana...

• Type: Conference
• Year: 1990
• Where: AAAI
• Authors: Gerald E. Peterson
• Keywords: AAAI 1990, Complete Set, Intelligent Agents, KB Algorithm, Left-hand Side