An AC-compatible Knuth-Bendix order

Konstantin Korovin, Andrei Voronkov

    Research output: Chapter in Book/Conference proceedingConference contribution

    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 languageEnglish
    Title of host publicationLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell
    EditorsF. Baader
    PublisherSpringer Nature
    Pages47-59
    Number of pages12
    Volume2741
    Publication statusPublished - 2003
    Event19th 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

    NameLecture Notes in Computer Science

    Conference

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

    Fingerprint

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

    Cite this