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.