Decreasing Diagrams and Relative Termination
Decreasing Diagrams and Relative Termination
复制标题
递减图和相对终止
DOI：
10.1007/s10817-011-9238-x
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Aart Middeldorp
中科院分区：
文献类型：
--
作者：
Nao Hirokawa;Aart Middeldorp
在这篇文章中，我们使用递减图技术来证明，左线性和局部合流项重写系统是合流的，如果关键对步骤相对终止于。我们进一步展示了如何编码的规则标签启发式减少图作为一个可满足性问题。这两种方法的实验数据。
In this article we use the decreasing diagrams technique to show that a left-linear and locally confluent term rewrite systemis confluent if the critical pair steps are relatively terminating with respect to. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are presented.