System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912426872537088 |
|---|---|
| author | Bartholomew, Michael Lee, Joohyung |
| author_facet | Bartholomew, Michael Lee, Joohyung |
| contents | 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 {\sc aspsmt2smt}, which implements this translation. The system uses ASP grounder {\sc gringo} and SMT solver {\sc z3}. {\sc gringo} partially grounds input programs while leaving some variables to be processed by {\sc z3}. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_10708 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers Bartholomew, Michael Lee, Joohyung Artificial Intelligence Logic in Computer Science 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 {\sc aspsmt2smt}, which implements this translation. The system uses ASP grounder {\sc gringo} and SMT solver {\sc z3}. {\sc gringo} partially grounds input programs while leaving some variables to be processed by {\sc z3}. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes. |
| title | System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2506.10708 |