CAREER: Principles, Practice, and Applications of Tabled Logic Programs

9702681许多实际问题，如程序的编译时分析、并发系统的验证、智能代理的规划和物理系统的诊断，都有一个共同的事实，即它们可以很容易地用逻辑来指定。然而，使用传统逻辑编程技术执行这种规范的尝试通常不会终止，因此是不切实际的。该项目旨在创建一个逻辑编程系统，它可以解决这些问题，并借鉴了最近在表式和约束逻辑编程方面的研究。表逻辑编程，特别是XSB系统，终止于大类程序，并允许在存在不一致信息的情况下通过其缺省否定的语义进行推理。约束逻辑编程允许将实数等理论中的问题声明性地表示出来并自动解决。该项目将以XSB为起点，为这两种范例建立统一的计算基础。对于并发系统验证和程序分析中的某些问题，基于C的大程序已经被数百条XSB规则取代，而不会降低效率。该项目将增加此类问题的数量，对于这些问题，基于逻辑的规范将导致高效、实用的系统。***

9702681 Many practical problems such as compile-time analysis of programs, verification of concurrent systems, planning by intelligent agents, and diagnosis of physical systems have in common the fact that they can be easily specified using logic. However, attempts to execute such specifications using traditional logic programming techniques usually do not terminate, and are thus impractical. This project seeks to create a logic programming system which can solve such problems and draws on recent research in tabled and constraint logic programming. Tabled logic programming, particularly the XSB system, terminates for large classes of programs, and permits reasoning in the presence of inconsistent information through its semantics for default negation. Constraint logic programming allows problems in theories such as the real numbers to be expressed declaratively and solved automatically. The project will create a unified computational basis for the two paradigms using XSB as a starting point. For certain problems in the verification of concurrent systems and in program analysis, large programs based on C already have been replaced with a few hundred XSB rules with no loss in efficiency. The project will increase the number of such problems for which a logic-based specification leads to an efficient, practical system. ***