包含算术谓词程序的自动终止分析

对于包含算术谓词的逻辑程序，证明终止性并不容易，因为整数的常规顺序不可调和。本文提出一种新方法，易于集成到 TermiLog 系统中用于自动终止分析，以此方法可以证明此类情况下的终止性。该方法包括以下步骤：首先，自动推导用于表示整数范围的有限抽象域。基于此抽象，对程序进行抽象解释。结果是抽象查询答案的一个有限数量的原子，这些原子用于扩展查询-映射配对技术。对于每个可能非终止的查询-映射配对，都会猜测一个有界（整数值）终止函数。如果遍历该配对会降低终止函数的值，则确定终止性。简单函数往往足以满足每个查询-映射配对的需求，这使我们的方法在使用单个终止函数覆盖所有循环（必须且不可避免地更复杂且难以自动猜测）的经典方法方面具有优势。值得注意的是，可以使用本方法自动证明 McCarthy 的 91 函数的终止性。总之，提出的方法基于将整数的有限抽象与查询-映射配对技术相结合，本质上能够将终止证明划分为几个案例，以便每个案例都足够简单，从而可以在 TermiLog 和类似系统的框架内自动完成整个终止性证明过程。