A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules
A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules
复制标题
自动证明一组重写规则终止的过程
DOI：
10.1007/3-540-15976-2_12
复制
发表时间：
1985
期刊：
影响因子：
--
通讯作者：
R. Forgaard
中科院分区：
文献类型：
--
作者：
David Detlefs;R. Forgaard
在本文中，我们提出了一个算法。Rithm可以自动证明多组重写规则的终止。用于证明重写规则集的终止的先前技术要么需要用户帮助来指导证明，要么限制性太强而不能普遍适用。除了在其本身的权利是有趣的，一个程序，证明终止自动是一个重要的一步，自动产生一组重写规则，从一组方程的过程的建设。
In this paper, we present an algo. rithm that can automatically prove the termination of many sets of rewrite rules. Previous techniques for proving termination of sets of rewrite rules have either required user help in guiding the proof, or have been too restrictive to be generally applicable. Besides being interesting in its own right, a procedure that proves termination automatically is an important step towards the construction of a procedure that automatically produces a convei'gent set of rewrite rules from a set o; equations.