System ASPMT2SMT: Computing ASPMT theories by SMT solvers

Michael Bartholomew, Joohyung Lee

Research output: Contribution to journalArticle

16 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 languageEnglish (US)
Pages (from-to)529-542
Number of pages14
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8761
StatePublished - Jan 1 2014

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this