Tabled Logic Programming in the Large

大型表逻辑编程

• 批准号: 9711386
• 负责人: IV Ramakrishnan
• 金额: $ 9.69万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-09-01 至 2000-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9711386&HistoricalAwards=false
• 关键词: Tabled; Logic; Programming; Large

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.

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