# Item

ITEM ACTIONSEXPORT

Released

Journal Article

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

##### 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.