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. ***