An AC-compatible Knuth-Bendix order

Konstantin Korovin, Andrei Voronkov

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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 languageEnglish
    Title of host publicationLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell
    EditorsF. Baader
    PublisherSpringer Nature
    Number of pages12
    Publication statusPublished - 2003
    Event19th International Conference on Automated Deduction - Miami Beach, FL
    Duration: 1 Jul 2003 → …

    Publication series

    NameLecture Notes in Computer Science


    Conference19th International Conference on Automated Deduction
    CityMiami Beach, FL
    Period1/07/03 → …
    Internet address


    Dive into the research topics of 'An AC-compatible Knuth-Bendix order'. Together they form a unique fingerprint.

    Cite this