Paper Info
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.
Year
DOI
Venue
2001
10.1007/3-540-45127-7_12
RTA
Keywords
Field
DocType
homogeneous linear inequality,rewrite rules,decision problem,rules r,verifying orientability,integer-valued kbo,polynomial time,ground instance,knuth-bendix order,real-valued kbo
Integer,Discrete mathematics,Decision problem,Weight function,Orientability,Automated theorem proving,Algorithm,Time complexity,Rule of inference,Linear inequality,Mathematics
Conference
ISBN
Citations 
PageRank 
3-540-42117-3
9
0.96
References 
Authors
13
2
Name
Order
Citations
PageRank
Konstantin Korovin128820.64
Andrei Voronkov22670225.46