通用逻辑程序模块化终止证明
计算机科学中的逻辑
2025-06-18 v2 编程语言
摘要
我们提出了一种用于证明通用逻辑程序（即包含否定形式的逻辑程序）终止的模块化方法。它基于可接受程序的概念，但允许我们以真正模块化的方式证明终止。我们考虑由层次结构组成的模块程序，为每个模块分别处理提供了证明终止的通用结果。对于某些特定意义上行为良好的程序，即 well-moded 或 well-typed 程序，我们推导出一种简单验证技术和一种迭代证明方法。一些例子表明，我们的方法允许大大简化证明过程。
引用
@article{arxiv.cs/0005018,
title = {On Modular Termination Proofs of General Logic Programs},
author = {Annalisa Bossi and Nicoletta Cocco and Sandro Etalle and Sabina Rossi},
journal= {arXiv preprint arXiv:cs/0005018},
year = {2025}
}
备注
29 pages. To appear in Theory and Practice of Logic Programming