Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
复制标题
Slothrop：使用现代终止检查器完成 Knuth-Bendix
DOI：
10.1007/11805618_22
复制
发表时间：
2006
影响因子：
1.1
通讯作者：
Edwin M. Westbrook
中科院分区：
文献类型：
--
作者：
Ian Wehrman;Aaron Stump;Edwin M. Westbrook
一个Knuth-Benzmann完成过程是参数化的减少订购用于确保终止中间和由此产生的重写系统。虽然原则上可以使用任何归约排序，但现代完成工具通常只实现Knuth-Benzinger和路径排序。因此，完备化可能产生决策过程的理论仅限于那些可以用单一路径顺序定向的理论。
在本文中，我们提出了一个变种的Knuth-Benziran完成过程中，没有顺序是假设。相反，我们依赖于一个现代的终止检查器来验证重写系统的终止。新的方法是正确的，如果它终止;由此产生的重写系统是收敛的，等价于输入理论。完备化不仅是地收敛的，而且是完全收敛的。我们提出了一个新的程序，Slothrop，自动获得这样的理论，不承认路径排序完成的实现。
A Knuth-Bendix completion procedure is parametrized by a reduction ordering used to ensure termination of intermediate and resulting rewriting systems. While in principle any reduction ordering can be used, modern completion tools typically implement only Knuth-Bendix and path orderings. Consequently, the theories for which completion can possibly yield a decision procedure are limited to those that can be oriented with a single path order.
In this paper, we present a variant on the Knuth-Bendix completion procedure in which no ordering is assumed. Instead we rely on a modern termination checker to verify termination of rewriting systems. The new method is correct if it terminates; the resulting rewrite system is convergent and equivalent to the input theory. Completions are also not just ground-convergent, but fully convergent. We present an implementation of the new procedure, Slothrop, which automatically obtains such completions for theories that do not admit path orderings.