Orienting rewrite rules with the Knuth-Bendix order

Korovin, Konstantin; Voronkov, Andrei

Local TagsRelease HistoryDetailsSummary

Orienting rewrite rules with the Knuth-Bendix order

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

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2DB3-3 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2DB4-1

Genre: Journal Article

Files

show Files

Locators

show

Creators

show

hide

Creators:
Korovin, Konstantin¹, Author
Voronkov, Andrei¹, Author

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

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.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2004-06-23Date issued: 2003

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: Peer

Identifiers: eDoc: 201879
Other: Local-ID: C1256104005ECAFC-989A18913FFAD6B3C1256E24003DB3B9-KorovinVoronkov:IC:2003

Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show

hide

Title: Information and Computation

Source Genre: Journal

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 183 Sequence Number: - Start / End Page: 165 - 186 Identifier: -