逻辑程序自动终止分析的通用框架
摘要
本文描述了一个用于逻辑程序自动终止分析的通用框架，其中我们所理解的“终止”是针对给定查询的LD树构建的分支的有限性。对从无限LD树的某个子集分支映射到有限集合的一般属性进行了证明。基于此结果，推导出了若干终止定理，方法是使用不同的有限集合。前两个定理分别针对谓词依赖图和原子依赖图给出。随后，对与程序相关的查询-映射对的通用结果进行了证明（参见 \cite{Sagiv,Lindenstrauss:Sagiv}）。\cite{Lindenstrauss:Sagiv:Serebrenik}中描述的{\em TermiLog}系统的正确性正是基于此。该系统无法证明涉及算术谓词的程序的终止，因为整数的通常顺序是不可调和的。 presented a new method, which can be easily incorporated in {\em TermiLog} or similar systems, which makes it possible to prove termination for programs involving arithmetic predicates. It is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing a termination proof into several cases, such that a simple termination function suffices for each case. Finally several possible extensions are outlined.
引用
@article{arxiv.cs/0012007,
title = {Kima - an Automated Error Correction System for Concurrent Logic Programs},
author = {Yasuhiro Ajiro and Kazunori Ueda},
journal= {arXiv preprint arXiv:cs/0012007},
year = {2007}
}
备注
In M. Ducasse (ed), proceedings of the Fourth International Workshop on Automated Debugging (AADEBUG 2000), August 2000, Munich. cs.SE/0010035