Orienting rewrite rules with the Knuth-Bendix order

Konstantin Korovin, Andrei Voronkov

    Research output: Contribution to journalArticlepeer-review

    Abstract

    We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability: given a system of rewrite rules R, does there exist an instance of KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given instance of KBO orients every ground instance of a given rewrite rule. This problem can also be reformulated as the problem of solving a single ordering constraint for the KBO. We prove that both problems can be solved in the time polynomial in the size of the input. The polynomial-time algorithm for orientability builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. We show that the orientability problem is P-complete. The polynomial-time algorithm for solving a single ordering constraint does not need to solve systems of linear inequalities and can be run in time O(n2). Also we show that if a system is orientable using a real-valued instance of KBO, then it is also orientable using an integer-valued instance of KBO. Therefore, all our results hold both for the integer-valued and the real-valued KBO.
    Original languageEnglish
    Pages (from-to)165-186
    Number of pages21
    JournalInformation and Computation
    Volume183
    Issue number2
    DOIs
    Publication statusPublished - 15 Jun 2003

    Keywords

    • Knuth-Bendix orders
    • Ordering constraints
    • Orientability
    • Term rewriting
    • Termination

    Fingerprint

    Dive into the research topics of 'Orienting rewrite rules with the Knuth-Bendix order'. Together they form a unique fingerprint.

    Cite this