RI: Small: Integrating Logic Based Declarative Programming Paradigms

该项目正在开发一种新的，强大的声明式编程范式，能够解决需要大量不同知识和使用不同推理方法的计算问题。这样的问题在实践中经常发生，但不能用更传统的声明式（或过程式）编程方法来解决。该研究包括开发用于表示各种类型的知识的语言，用于推理这些知识的算法和系统，以及使用语言和系统解决各种计算问题的方法。我们的声明式编程方法将整合答案集编程（ASP），约束编程（CP），基于布尔可满足性（SAT）和可满足性模理论（SMT）的编程方法的思想，并具有包括溯因和概率推理的长期目标。该方法将在具有挑战性的应用领域中的问题上进行测试，例如航天飞机控制器的决策支持系统，具有复杂授权和义务政策的安全软件系统，以及能够基于非平凡领域知识进行规划和调度的系统。

The project is developing a new, powerful paradigm for declarative programming, capable of solving computational problems that require a large amount of diverse knowledge and use of different reasoning methods. Such problems frequently occur in practice but cannot be solved by more traditional methods of declarative (or procedural) programming. The research includes the development of a language for representing various types of knowledge, algorithms and systems for reasoning about this knowledge, and a methodology of using the language and the systems for solving a large variety of computational problems. Our approach to declarative programming will integrate the ideas from Answer Set Programming (ASP), Constraint Programming (CP), programming methods based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theory (SMT), and with a longer-term goal of including abductive and probabilistic reasoning as well. The approach will be tested on problems in challenging application domains such as a decision support system for space shuttle controllers, secure software systems with complex authorization and obligation policies, and systems capable of planning and scheduling based on non-trivial domain knowledge.