TY - JOUR
T1 - System ASPMT2SMT
T2 - Computing ASPMT theories by SMT solvers
AU - Bartholomew, Michael
AU - Lee, Joohyung
N1 - Funding Information:
Acknowledgements. We are grateful to the anonymous referees for their useful comments. This work was partially supported by the National Science Foundation under Grant IIS-1319794 and by the South Korea IT R&D program MKE/KIAT 2010-TD-300404-001.
Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable models of ASPMT programs. In this paper we present a compiler called ASPSMT2SMT, which implements this translation. The system uses ASP grounder GRINGO and SMT solver Z3. GRINGO partially grounds input programs while leaving some variables to be processed by Z3. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.
AB - Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable models of ASPMT programs. In this paper we present a compiler called ASPSMT2SMT, which implements this translation. The system uses ASP grounder GRINGO and SMT solver Z3. GRINGO partially grounds input programs while leaving some variables to be processed by Z3. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.
UR - http://www.scopus.com/inward/record.url?scp=84921734782&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84921734782&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-11558-0_37
DO - 10.1007/978-3-319-11558-0_37
M3 - Article
AN - SCOPUS:84921734782
VL - 8761
SP - 529
EP - 542
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
SN - 0302-9743
ER -