arXiv Open Access 2025

Anthem 2.0: Automated Reasoning for Answer Set Programming

Jorge Fandinno Christoph Glinzer Zachary Hansen Jan Heuer Yuliya Lierler +3 lainnya

Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

cs.LO

Penulis (8)

Jorge Fandinno

Christoph Glinzer

Zachary Hansen

Jan Heuer

Yuliya Lierler

Vladimir Lifschitz

Torsten Schaub

Tobias Stolzmann

Format Sitasi

APA MLA BibTeX

Fandinno, J., Glinzer, C., Hansen, Z., Heuer, J., Lierler, Y., Lifschitz, V. et al. (2025). Anthem 2.0: Automated Reasoning for Answer Set Programming. https://arxiv.org/abs/2507.11704

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2025
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓