Datensatz

Zusammenfassung

We introduce a family of AC-compatible Knuth-Bendix simplification orderings which are AC-total on ground terms. Our orderings preserve attractive features of the original Knuth-Bendix orderings such as polynomial algorithm for comparing terms; the orderings admit computationally efficient approximations like checking weights of terms; and prefer light terms to heavy ones. This makes them especially suited for automated deduction where efficient treatment of orderings is desirable.