Abstract
We introduce a family of AC-compatible Knuth-Bendix simplification orders which are AC-total on ground terms. Our orders preserve attractive features of the original Knuth-Bendix orders such as existence of a polynomial-time algorithm for comparing terms; computationally efficient approximations, for instance comparing weights of terms; and preference of light terms over heavy ones. This makes these orders especially suited for automated deduction where efficient algorithms on orders are desirable.
Original language | English |
---|---|
Title of host publication | Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell |
Editors | F. Baader |
Publisher | Springer Nature |
Pages | 47-59 |
Number of pages | 12 |
Volume | 2741 |
Publication status | Published - 2003 |
Event | 19th International Conference on Automated Deduction - Miami Beach, FL Duration: 1 Jul 2003 → … http://dblp.uni-trier.de/db/conf/cade/cade2003.html#RiazanovV03http://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV03.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV03 |
Publication series
Name | Lecture Notes in Computer Science |
---|
Conference
Conference | 19th International Conference on Automated Deduction |
---|---|
City | Miami Beach, FL |
Period | 1/07/03 → … |
Internet address |