| 9:00 | Ilkka Niemelä |
| Integrating Answer Set Programming and Satisfiability Modulo Theories |
| 10:00 | Yuliya Lierler and Yuanlin Zhang |
| A transition system for AC language algorithms (paper) | |
| 10:30 | Yuliya Lierler, Shaden Smith, Mirek Truszczynski and Alex Westlund |
| Weighted-Sequence Problem: ASP vs CASP and Declarative vs Problem Oriented Solving (paper) |
| 11:30 | Weijun Zhu |
| A New Algorithm for P-log Inference Engine (paper) | |
| 12:00 | Alex Brik and Jeffrey Remmel |
| Computing Stable Models of Logic Programs Using Metropolis Type Algorithms (paper) | |
| 12:30 | Marcello Balduccini and Yuliya Lierler |
| ASP-Based Problem Solving with Cutting-Edge Tools (paper) |
| 14:00 | Michael Gelfond |
| Some Thoughts on the Development of Action Theories |
| 15:00 | Mario Alviano, Wolfgang Faber and Stefan Woltran |
| Complexity of Super-Coherence Problems in ASP (paper) | |
| 15:30 | Vladimir Lifschitz |
| Logic Programs with Intensional Functions (Preliminary Report) (paper) |
Ilkka Niemelä, Aalto University, Finland.
In this talk we consider the problem of integrating answer set
programming (ASP) and satisfiability modulo theories (SMT). We discuss a
characterization of stable models of logic programs based on Clark's
completion and simple difference constraints. The characterization
leads to a method of translating a set of ground logic program rules to a
linear size theory in difference logic, i.e. propositional logic extended with
difference constraints between two integer variables, such that stable
models of the rule set correspond to satisfying assignments of the
resulting theory in difference logic. Many of the state-of-the-art
SMT solvers support directly difference logic. This opens up interesting
possibilities. On one hand, any solver supporting difference logic can
be used immediately without modifications as an ASP solver for computing
stable models of a logic program by translating the program to a theory
in difference logic. On the other hand, SMT solvers typically support
also other extensions of propositional logic such as linear real and
integer arithmetic, fixed-size bit vectors, arrays, and uninterpreted
functions. This suggests interesting opportunities to extend ASP
languages with such constraints and to provide effective solver support
for the extensions. Using the translation an extended language
including logic program rules and, for example, linear real arithmetic
can be translated to an extension of propositional logic supported by
current SMT solvers. We discuss the effectiveness of state-of-the-art
SMT solvers as ASP solvers and the possibilities of developing extended
ASP languages based on SMT solver technology.
Michael Gelfond, Texas Tech University.
In this talk I'll discuss some history and some recent developments in the Theory of Action and Change -- the area which has been one of my major research interests for more than 25 years, and which is very closely related to Logic Programming.
I describe some questions I attempted to address in this research, the choices I was confronted with, and methodological assumptions used in the process.
I hope that this story may be useful
for newcomers to the field (and even for those who worked in it for
some time).