{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T13:00:18Z","timestamp":1761310818267,"version":"build-2065373602"},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2025,9,18]],"date-time":"2025-09-18T00:00:00Z","timestamp":1758153600000},"content-version":"unspecified","delay-in-days":79,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2025,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>ANTHEM 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of CLINGO \u2019s 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\u2019s capabilities. We demonstrate how to use ANTHEM 2.0 effectively and interpret its results.<\/jats:p>","DOI":"10.1017\/s1471068425100112","type":"journal-article","created":{"date-parts":[[2025,9,18]],"date-time":"2025-09-18T06:35:41Z","timestamp":1758177341000},"page":"668-684","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["ANTHEM 2.0: Automated Reasoning for Answer Set Programming"],"prefix":"10.1017","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3917-8717","authenticated-orcid":false,"given":"JORGE","family":"FANDINNO","sequence":"first","affiliation":[{"name":"University of Nebraska Omaha"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8447-4048","authenticated-orcid":false,"given":"ZACHARY","family":"HANSEN","sequence":"additional","affiliation":[{"name":"University of Nebraska Omaha"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6146-623X","authenticated-orcid":false,"given":"YULIYA","family":"LIERLER","sequence":"additional","affiliation":[{"name":"University of Nebraska Omaha"}]},{"given":"CHRISTOPH","family":"GLINZER","sequence":"additional","affiliation":[{"name":"University of Potsdam"}]},{"given":"JAN","family":"HEUER","sequence":"additional","affiliation":[{"name":"University of Potsdam"}]},{"given":"TORSTEN","family":"SCHAUB","sequence":"additional","affiliation":[{"name":"University of Potsdam"}]},{"given":"TOBIAS","family":"STOLZMANN","sequence":"additional","affiliation":[{"name":"University of Potsdam"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6051-7907","authenticated-orcid":false,"given":"VLADIMIR","family":"LIFSCHITZ","sequence":"additional","affiliation":[{"name":"University of Texas at Austin"}]}],"member":"56","published-online":{"date-parts":[[2025,9,18]]},"reference":[{"key":"S1471068425100112_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/11546207_43"},{"key":"S1471068425100112_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000150"},{"key":"S1471068425100112_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068425100112_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068420000344"},{"key":"S1471068425100112_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S147106842300039X"},{"key":"S1471068425100112_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20528-7_20"},{"key":"S1471068425100112_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2017.02.002"},{"key":"S1471068425100112_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43619-2"},{"key":"S1471068425100112_ref4","doi-asserted-by":"publisher","DOI":"10.24963\/kr.2023\/24"},{"key":"S1471068425100112_ref10","first-page":"42","volume-title":"Sitzungsberichte der Preussischen Akademie der Wissenschaften","author":"Heyting","year":"1930"},{"key":"S1471068425100112_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00675-3_16"},{"key":"S1471068425100112_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45329-6_31"},{"key":"S1471068425100112_ref9","unstructured":"Heuer, J. 2020. Automated verification of equivalence properties in advanced logic programs. Bachelor\u2019s thesis, University of Potsdam. https:\/\/arxiv.org\/abs\/2310.19806."},{"key":"S1471068425100112_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/383779.383783"},{"key":"S1471068425100112_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89982-2_49"},{"key":"S1471068425100112_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-006-9028-z"},{"key":"S1471068425100112_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"S1471068425100112_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24609-1_30"},{"key":"S1471068425100112_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9407-7"},{"key":"S1471068425100112_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30227-8_69"},{"key":"S1471068425100112_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068423000200"},{"key":"S1471068425100112_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-75775-5_28"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068425100112","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T12:56:27Z","timestamp":1761310587000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068425100112\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,7]]}},"alternative-id":["S1471068425100112"],"URL":"https:\/\/doi.org\/10.1017\/s1471068425100112","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2025,7]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}