ASPMT2SMT swMATH ID: 13280 Software Authors: Bartholomew, Michael; Lee, Joohyung Description: System ASPMT2SMT: computing ASPMT theories by SMT solvers. 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. Homepage: http://reasoning.eas.asu.edu/aspmt/ Related Software: Clingcon; DLV2; ezcsp; Clingo; WASP; clasp; z3; MiniSat; Potassco; Chaff; Datalog; GASP; Gringo; CCalc; dReal; PDDL; QEPCAD; f2lp; Cplus2ASP Cited in: 5 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year System aspmt2smt: computing ASPMT theories by SMT solvers. Zbl 1432.68055Bartholomew, Michael; Lee, Joohyung 2014 all top 5 Cited by 9 Authors 2 Bartholomew, Michael 2 Dodaro, Carmine 2 Lee, Joohyung 2 Ricca, Francesco 1 Bhatt, Mehul 1 Cuteri, Bernardo 1 Schüller, Peter 1 Schultz, Carl R. 1 Wałęga, Przemysław Andrzej Cited in 2 Serials 3 Theory and Practice of Logic Programming 1 Artificial Intelligence Cited in 1 Field 5 Computer science (68-XX) Citations by Year