English

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Orienting rewrite rules with the Knuth-Bendix order

MPS-Authors
/persons/resource/persons44827

Korovin,  Konstantin
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45678

Voronkov,  Andrei
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Korovin, K., & Voronkov, A. (2003). Orienting rewrite rules with the Knuth-Bendix order. Information and Computation, 183, 165-186.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2DB3-3
Abstract
We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is \emph{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(n^2)$. 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.