Answer Set Programming Modulo Theories and Reasoning about Continuous Changes
Abstract
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.
Cite
@article{arxiv.2507.04299,
title = {Answer Set Programming Modulo Theories and Reasoning about Continuous Changes},
author = {Joohyung Lee and Yunsong Meng},
journal= {arXiv preprint arXiv:2507.04299},
year = {2025}
}
Comments
In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), pages 990-996, 2013