de.mpg.escidoc.pubman.appbase.FacesBean
English

# Item

ITEM ACTIONSEXPORT

Released

Journal Article

#### Orienting rewrite rules with the Knuth-Bendix order

##### MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44827

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

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45678

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

##### Locator
There are no locators available
##### Fulltext (public)
There are no public fulltexts available
##### 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: http://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.