Tabled Logic Programming in the Large

一般逻辑程序的表解析已被证明在声明性地解决复杂应用程序时是有效的，包括通过模型检查进行程序验证，以及用于优化编译器的程序分析。使用XSB表逻辑编程系统构建了上述应用程序的高效实现，它的性能至少与现有实现一样好，这些实现由用低级语言编写的大得多的程序组成。该项目旨在提高表逻辑编程系统的表现力、效率和易用性。该项目的主要目标是：(a)研究约束求解与表解析的相互作用，这种组合大大增加了表逻辑编程系统的表达能力。(b)设计优化表约束逻辑规划系统的技术，将传统的因式分解和索引扩展到约束，并通过选择性表。(c)构建用于表逻辑程序高级调试的工具。表和约束分别为传统逻辑编程系统引入了一个新的声明性层次。表和约束的组合支持对无法使用任何一种单独范例以声明方式解决的问题进行编码。因此，表约束逻辑编程有望成为实现声明性编程理想的重要一步。

Tabled resolution for general logic programs has been shown to be effective in declaratively solving complex applications, including program verification through model checking, and program analysis for optimizing compilers. Efficient implementations of the above applications have been built using the XSB tabled logic programming system, which perform at least as well as existing implementations consisting of much larger programs written in lower level languages. The project is aimed at improving the expressiveness, efficiency and ease of use of tabled logic programming systems. The main goals of this project are: (a) To study the interaction of constraint solving with tabled resolution, a combination that considerably increases the expressiveness of tabled logic programming systems. (b)To design techniques for optimizing tabled constraint logic programming systems by extending traditional factoring and indexing to constraints, and by selective tabling. (c) To construct tools for high-level debugging of tabled logic programs. Tabling and constraints have both separately introduced a new level of declarativeness to traditional logic programming systems. The combination of tabling and constraints enables encoding of problems that cannot be solved declaratively using either individual paradigm. Tabled constraint logic programming thus promises to be a significant step towards realizing the ideal of declarative programming.