Journal Article @Article Artikel in Fachzeitschrift
 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Goto entry point

 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: (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},