Anthem 2.0: Automated Reasoning for Answer Set Programming
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918287336538112 |
|---|---|
| author | Fandinno, Jorge Glinzer, Christoph Hansen, Zachary Heuer, Jan Lierler, Yuliya Lifschitz, Vladimir Schaub, Torsten Stolzmann, Tobias |
| author_facet | Fandinno, Jorge Glinzer, Christoph Hansen, Zachary Heuer, Jan Lierler, Yuliya Lifschitz, Vladimir Schaub, Torsten Stolzmann, Tobias |
| contents | Anthem 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of Clingo's input language named mini-gringo, which includes arithmetic operations and simple choice rules but not aggregates. It can translate logic programs into formula representations in the logic of here-and-there, and analyze properties of logic programs such as tightness. Most importantly, Anthem 2.0 can support program verification by invoking first-order theorem provers to confirm that a program adheres to a first-order specification, or to establish strong and external equivalence of programs. This paper serves as an overview of the system's capabilities. We demonstrate how to use Anthem 2.0 effectively and interpret its results. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_11704 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Anthem 2.0: Automated Reasoning for Answer Set Programming Fandinno, Jorge Glinzer, Christoph Hansen, Zachary Heuer, Jan Lierler, Yuliya Lifschitz, Vladimir Schaub, Torsten Stolzmann, Tobias Logic in Computer Science I.2.3 Anthem 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of Clingo's input language named mini-gringo, which includes arithmetic operations and simple choice rules but not aggregates. It can translate logic programs into formula representations in the logic of here-and-there, and analyze properties of logic programs such as tightness. Most importantly, Anthem 2.0 can support program verification by invoking first-order theorem provers to confirm that a program adheres to a first-order specification, or to establish strong and external equivalence of programs. This paper serves as an overview of the system's capabilities. We demonstrate how to use Anthem 2.0 effectively and interpret its results. |
| title | Anthem 2.0: Automated Reasoning for Answer Set Programming |
| topic | Logic in Computer Science I.2.3 |
| url | https://arxiv.org/abs/2507.11704 |