Instructor: Vladimir Lifschitz
Answer set programming (ASP) is a form of logic programming that involves the use of answer set solvers -- software systems for generating stable models. Stable models were introduced in 1988 for the purpose of defining a declarative semantics of negation as failure in logic programming. The first system for generating stable models of a logic program, called SMODELS, was created in 1996. It operates by grounding the program -- transforming it into a program without variables that has the same stable models -- and then performing search using algorithms similar to those used in SAT solvers. Other answer set solvers, such as DLV and CLINGO, operate in a similar way.
The earliest example of what is now called answer set programming is found in the 1997 paper that described its approach to AI planning as follows: we encode planning problems in such a way that stable models of the encodings correspond to valid sequences of actions. It soon became clear that encoding solutions to a problem by stable models and then calling an answer set solver to find them is a general declarative programming paradigm, not limited to planning.
Answer set programming has been used to solve computational problems as diverse as reconstructing evolutionary trees in biology and linguistics; configuring railway safety systems and products in automotive industry; finding answers to biomedical queries; generating plans for the Reaction Control System of the Space Shuttle; haplotype inference in genetics; optimizing positions of valves in a water distribution system; team building in the port of Gioia Tauro in Italy.
The process of creating an ASP program can be divided into two stages. In the knowledge representation stage, we represent the domain by a logic program such that its stable models match the objects that we want to find. If we are lucky, then the solver will be able to find a stable model of this program, so that the problem at hand will be solved. But many search problems (for instance, planning) are intrinsically hard, and generating a stable model may take too long. It may even happen that the search process never starts, because grounding the program requires too much time or space, or because an attempt to ground it causes the grounder to generate an "unsafe variable" message. In such cases, the improvement stage is required: we modify the program to make it safe for grounding and efficient for search. The modified program will share with the original version its main property: its stable models will correspond to solutions. In this sense, improving a program is an equivalent transformation.
The topic of this tutorial is the use of formal methods -- mathematical proofs and automated reasoning tools -- in the development of correct and efficient ASP programs. During the improvement stage of program development, formal methods can help us verify that each improvement step is indeed an equivalent transformation. We will review recent research related to this idea, including the definition of equivalence of ASP programs with respect to a user guide and the design of the proof assistant ANTHEM.
The tutorial is intended for graduate students and researchers interested in logic-based AI, knowledge representation, reasoning about actions, declarative programming, and automated reasoning. It consists of two parts: