Solving Term Inequalities

9 years 10 months ago
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...
Gerald E. Peterson
Added 06 Nov 2010
Updated 06 Nov 2010
Type Conference
Year 1990
Where AAAI
Authors Gerald E. Peterson
Comments (0)