Answer set programming (ASP) is a declarative paradigm for the design and implementation of knowledge intensive applications, especially those that involve combinatorial search. It grew out of early work on the semantics of negation as failure, nonmonotonic reasoning and satisfiability solvers. ASP is used today in many areas of science and technology.
The process of creating an ASP program involves representing a domain in the language of an answer set solver, and then making that representation safe for grounding and efficient for search. Attendees will see how methods of mathematical logic can be used to verify that improvements made in the second stage of this process are indeed equivalent transformations. They will learn about the operation of the proof assistant anthem, which is designed for the purpose of facilitating proofs of this kind. The tutorial is intended for graduate students and researchers interested in logic-based AI, knowledge representation, reasoning about actions, declarative programming, and automated reasoning.
