Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Korovin, Konstantin
Voronkov, Andrei		dblp
dblp
Not MPG Author(s):
Voronkov, Andrei

BibTeX cite key*:

KorovinVoronkov:IC:2003

Title

Title*:

Orienting rewrite rules with the Knuth-Bendix order

Journal

Journal Title*:

Information and Computation
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Elsevier
Publisher's URL:

http://www.elsevier.com/

Publisher's
Address:

Amsterdam, The Netherlands
ISSN:


Vol, No, pp, Date

Volume*:

183
Number:

2

Publishing Date:

2003

Pages*:

165-186
Number of
VG Pages:

22

Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) 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.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Intranet

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
popular
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort, CCL bibliography


BibTeX Entry:
@ARTICLE{KorovinVoronkov:IC:2003,
AUTHOR = {Korovin, Konstantin and Voronkov, Andrei},
 TITLE = {Orienting rewrite rules with the {Knuth-Bendix} order},
 JOURNAL = {Information and Computation},
 PUBLISHER = {Elsevier},
 YEAR = {2003},
 NUMBER = {2},
 VOLUME = {183},
 PAGES = {165--186},
 ADDRESS = {Amsterdam, The Netherlands},
}

Entry last modified by Viorica Sofronie-Stokkermans, 01/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Konstantin Korovin		Created
01/23/2004 12:13:57 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Viorica Sofronie-Stokkermans
Anja Becker
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
06/23/2004 02:35:08 PM
21.06.2004 16:08:02
17.06.2004 17:55:18
17.06.2004 14:31:41
17.06.2004 14:29:04