Using ATMS to Efficiently Verify the Termination of Rewrite Rule Programs
Using ATMS to Efficiently Verify the Termination of Rewrite Rule Programs
复制标题
利用ATMS高效验证重写规则程序的终止
DOI：
10.1142/s0218194092000257
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
A. Ohuchi
中科院分区：
文献类型：
--
作者：
M. Kurihara;Hisashi Kondo;A. Ohuchi
基于假设的真值维护系统（ATMS）已经成为人工智能问题求解器中功能强大且广泛使用的工具。在本文中，我们应用ATMS验证终止的计算机程序编写为一组重写规则。与传统的基于普通回溯的方法相比，该方法利用ATMS的避免无效回溯、重新发现推理和重新发现矛盾的能力，大大提高了整体效率.我们的工作的独创性在于在软件工程问题中的ATMS的实际使用，并在终止验证器和ATMS之间的通信协议。
Assumption-based truth maintenance systems (ATMS) have become powerful and widely used tools in artificial intelligence problem solvers. In this paper, we apply ATMS to verification of termination of computer programs written as a set of rewrite rules. Compared with the traditional methods based on the ordinary backtracking, our method can greatly improve the overall efficiency by virtue of the ATMS's ability to avoid futile backtracking, rediscovering inferences, and rediscovering contradictions. The originality of our work lies in the practical use of the ATMS in a software engineering problem and in the communication protocol between the termination verifier and the ATMS.