具有表格化的逻辑程序的终止证明
摘要：表格化逻辑编程受到逻辑编程社区越来越多的关注。它避免了SLD执行的许多缺点，并为逻辑程序提供了一种更灵活和通常极高效的执行机制。与基于SLD-resolution的执行相比，表格化逻辑程序的执行更频繁地终止。在本文中，我们引入了两个关于带Tabling的逻辑编程的普遍终止概念：准终止和（更强的）LG-终止概念。我们提出了这两个终止概念的充分条件，即准可接受性和LG-可接受性，并且我们还证明了在Tabling选择良好的情况下，这些条件也是必要的。从这些条件出发，我们给出了模块化终止证明，即能够将单独程序的终止证明组合起来得到组合程序的终止证明。最后，在模式信息存在的情况下，我们给出了自动证明终止的基础条件，这可以通过约束来实现。
作者：Sofie Verbaeten, Danny De Schreye, Konstantinos Sagonas
论文ID：cs/0003045
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23