cTI：用于 ISO-Prolog 的约束基终止推理工具
编程语言
2007-05-23 v1
摘要
我们提出了 cTI，这是第一个实现通用左终止（universal left-termination）推理的逻辑程序系统。终止推理概括了终止分析与检查。传统上，终止分析器试图证明给定查询类的终止性。必须向系统提供此类查询的类，例如通过用户注释。此外，分析每次更新感兴趣查询类的方式都需要重新进行。相反，终止推理无需用户注释或重新计算。在这种方法中，所有谓词的终止类一次性推理。我们描述了 cTI 的体系结构，并报告了该系统进行了广泛的实验评估，涵盖了许多来自逻辑程序终止文献的经典示例以及若干规模和复杂度较大的 Prolog 程序。
关键词
引用
@article{arxiv.cs/0309028,
title = {cTI: A constraint-based termination inference tool for ISO-Prolog},
author = {Fred Mesnard and Roberto Bagnara},
journal= {arXiv preprint arXiv:cs/0309028},
year = {2007}
}
备注
16 pages, 3 tables, to appear on "Theory and Practice of Logic Programming"