Verifying orientability of rewrite rules using the Knuth-Bendix order

Konstantin Korovin; Andrei Voronkov

doi:10.1007/3-540-45127-7_12

Verifying orientability of rewrite rules using the Knuth-Bendix order

Research output: Chapter in Book/Conference proceeding › Conference contribution

Abstract

We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability : given a system of rewrite rules R, does there exist some KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given KBO orients a 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 polynomial time. The algorithm builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. Also we show that if a system is orientable using a real-valued KBO, then it is also orientable using an integer-valued KBO. © Springer-Verlag Berlin Heidelberg 2001.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	137-153
Number of pages	16
Volume	2051
ISBN (Print)	3540421173, 9783540421177
DOIs	https://doi.org/10.1007/3-540-45127-7_12
Publication status	Published - 2001
Event	12th International Conference on Rewriting Techniques and Applications, RTA 2001 - Utrecht Duration: 1 Jul 2001 → … http://dblp.uni-trier.de/db/conf/rta/rta2001.html#KorovinV01http://dblp.uni-trier.de/rec/bibtex/conf/rta/KorovinV01.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/rta/KorovinV01

Publication series

Name	Lecture Notes in Computer Science

Conference

Conference	12th International Conference on Rewriting Techniques and Applications, RTA 2001
City	Utrecht
Period	1/07/01 → …
Internet address	http://dblp.uni-trier.de/db/conf/rta/rta2001.html#KorovinV01http://dblp.uni-trier.de/rec/bibtex/conf/rta/KorovinV01.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/rta/KorovinV01

Access to Document

10.1007/3-540-45127-7_12

Cite this

Korovin, K., & Voronkov, A. (2001). Verifying orientability of rewrite rules using the Knuth-Bendix order. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci. (Vol. 2051, pp. 137-153). (Lecture Notes in Computer Science). Springer Nature. https://doi.org/10.1007/3-540-45127-7_12

@inproceedings{ca89a85ea4d941d49ecfe0d4fabae184,

title = "Verifying orientability of rewrite rules using the Knuth-Bendix order",

abstract = "We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability : given a system of rewrite rules R, does there exist some KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given KBO orients a 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 polynomial time. The algorithm builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. Also we show that if a system is orientable using a real-valued KBO, then it is also orientable using an integer-valued KBO. {\textcopyright} Springer-Verlag Berlin Heidelberg 2001.",

author = "Konstantin Korovin and Andrei Voronkov",

year = "2001",

doi = "10.1007/3-540-45127-7_12",

language = "English",

isbn = "3540421173",

volume = "2051",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "137--153",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

address = "United States",

note = "12th International Conference on Rewriting Techniques and Applications, RTA 2001 ; Conference date: 01-07-2001",

url = "http://dblp.uni-trier.de/db/conf/rta/rta2001.html#KorovinV01http://dblp.uni-trier.de/rec/bibtex/conf/rta/KorovinV01.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/rta/KorovinV01",

}

Korovin, K & Voronkov, A 2001, Verifying orientability of rewrite rules using the Knuth-Bendix order. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 2051, Lecture Notes in Computer Science, Springer Nature, pp. 137-153, 12th International Conference on Rewriting Techniques and Applications, RTA 2001, Utrecht, 1/07/01. https://doi.org/10.1007/3-540-45127-7_12

Verifying orientability of rewrite rules using the Knuth-Bendix order. / Korovin, Konstantin; Voronkov, Andrei.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 2051 Springer Nature, 2001. p. 137-153 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Conference proceeding › Conference contribution

TY - GEN

T1 - Verifying orientability of rewrite rules using the Knuth-Bendix order

AU - Korovin, Konstantin

AU - Voronkov, Andrei

PY - 2001

Y1 - 2001

N2 - We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability : given a system of rewrite rules R, does there exist some KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given KBO orients a 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 polynomial time. The algorithm builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. Also we show that if a system is orientable using a real-valued KBO, then it is also orientable using an integer-valued KBO. © Springer-Verlag Berlin Heidelberg 2001.

AB - We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability : given a system of rewrite rules R, does there exist some KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given KBO orients a 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 polynomial time. The algorithm builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. Also we show that if a system is orientable using a real-valued KBO, then it is also orientable using an integer-valued KBO. © Springer-Verlag Berlin Heidelberg 2001.

U2 - 10.1007/3-540-45127-7_12

DO - 10.1007/3-540-45127-7_12

M3 - Conference contribution

SN - 3540421173

SN - 9783540421177

VL - 2051

T3 - Lecture Notes in Computer Science

SP - 137

EP - 153

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 12th International Conference on Rewriting Techniques and Applications, RTA 2001

Y2 - 1 July 2001

ER -

Verifying orientability of rewrite rules using the Knuth-Bendix order

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this