System ASPMT2SMT: Computing ASPMT theories by SMT solvers

Michael Bartholomew; Joohyung Lee

doi:10.1007/978-3-319-11558-0_37

System ASPMT2SMT: Computing ASPMT theories by SMT solvers

Michael Bartholomew, Joohyung Lee

Research output: Contribution to journal › Article › peer-review

19 Scopus citations

Abstract

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.

Original language	English (US)
Pages (from-to)	529-542
Number of pages	14
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8761
DOIs	https://doi.org/10.1007/978-3-319-11558-0_37
State	Published - 2014

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-11558-0_37

Fingerprint Dive into the research topics of 'System ASPMT2SMT: Computing ASPMT theories by SMT solvers'. Together they form a unique fingerprint.

Cite this

@article{1e82052516f04586abee25367fb40b7d,

title = "System ASPMT2SMT: Computing ASPMT theories by SMT solvers",

abstract = "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.",

author = "Michael Bartholomew and Joohyung Lee",

year = "2014",

doi = "10.1007/978-3-319-11558-0_37",

language = "English (US)",

volume = "8761",

pages = "529--542",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - System ASPMT2SMT

T2 - Computing ASPMT theories by SMT solvers

AU - Bartholomew, Michael

AU - Lee, Joohyung

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 -