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.
