Name
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. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/978-3-540-45085-6_5 | Lecture Notes in Artificial Intelligence |
Keywords | Field | DocType |
automated deduction | Discrete mathematics,Compatibility (mechanics),Computer science,Automated theorem proving,Algorithm,Time complexity,Polynomial method,Equational theory | Conference |
Volume | ISSN | Citations |
2741 | 0302-9743 | 3 |
PageRank | References | Authors |
0.37 | 18 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Konstantin Korovin | 1 | 288 | 20.64 |
| Andrei Voronkov | 2 | 2670 | 225.46 |
| franz baader | 3 | 34 | 2.97 |