Answer Set Programming Modulo Theories and Reasoning about Continuous Changes
This work addresses the challenge of modeling continuous changes in AI reasoning systems, which is incremental as it builds on existing ASP and SMT methods.
The paper tackles the problem of integrating answer set programming (ASP) with satisfiability modulo theories (SMT) to create ASPMT, a framework for reasoning about continuous changes, and demonstrates its application by enhancing the action language C+ to handle both discrete and continuous changes, showing that SMT solvers can compute the language and represent cumulative effects on continuous resources.
Answer Set Programming Modulo Theories (ASPMT) is a new framework of tight integration of answer set programming (ASP) and satisfiability modulo theories (SMT). Similar to the relationship between first-order logic and SMT, it is based on a recent proposal of the functional stable model semantics by fixing interpretations of background theories. Analogously to a known relationship between ASP and SAT, ``tight'' ASPMT programs can be translated into SMT instances. We demonstrate the usefulness of ASPMT by enhancing action language C+ to handle continuous changes as well as discrete changes. We reformulate the semantics of C+ in terms ofASPMT, and show that SMT solvers can be used to compute the language. We also show how the language can represent cumulative effects on continuous resources.