Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

AAAI

1990

1990

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

Related Content

Added |
06 Nov 2010 |

Updated |
06 Nov 2010 |

Type |
Conference |

Year |
1990 |

Where |
AAAI |

Authors |
Gerald E. Peterson |

Comments (0)