Answer set programming (ASP) is a successful declarative programming method oriented towards solving combinatorial and knowledge intensive problems. It has well-developed foundations, efficient reasoning systems, and a methodology of use tested on a number of industrial applications. The relationship between ASP and propositional satisfiability (SAT) has led to a method of computing answer sets using SAT solvers and techniques adapted from SAT.

Some recent extensions of ASP are to overcome the propositional setting of ASP by extending its mathematical foundation and integrating ASP with other computing paradigms. The tutorial will cover “Answer Set Programming Modulo Theories”, which tightly integrates ASP with Satisfiability Modulo Theories (SMT), thereby overcoming some of the computational limitations of ASP and some of the modeling limitations of SMT. A high level action language based on ASPMT allows for succinct representation of hybrid transition systems, where discrete changes and continuous changes coexist. In a broader sense, ASPMT covers an extension of ASP combined with any external computation sources.

The target audience is those who are interested in declarative problem solving methods, recent developments in ASP and SMT, and their relations. Basic knowledge of first-order logic will be assumed, but no prior knowledge of ASP and SMT is required.

Slides

Software:

1. • aspmt2smt  http://reasoning.eas.asu.edu/aspmt
   

2. • mvsm  http://reasoning.eas.asu.edu/mvsm
   

Tutorial Speaker: Joohyung Lee (joolee (at) asu.edu) is an associate professor at Arizona State University. His research interests are in knowledge representation, logic programming, commonsense reasoning, and computational logic. He received a Ph.D. from the University of Texas at Austin. One of his papers on ASP received an Honorable Mention for the Outstanding Paper Award at AAAI 2004.