{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,29]],"date-time":"2026-06-29T14:02:24Z","timestamp":1782741744222,"version":"3.54.5"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T00:00:00Z","timestamp":1600646400000},"content-version":"unspecified","delay-in-days":20,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2020,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.<\/jats:p>","DOI":"10.1017\/s1471068420000344","type":"journal-article","created":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T05:25:42Z","timestamp":1600665942000},"page":"735-750","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":26,"title":["Verifying Tight Logic Programs with anthem and vampire"],"prefix":"10.1017","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3917-8717","authenticated-orcid":false,"given":"JORGE","family":"FANDINNO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6051-7907","authenticated-orcid":false,"given":"VLADIMIR","family":"LIFSCHITZ","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5902-4152","authenticated-orcid":false,"given":"PATRICK","family":"L\u00dcHNE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7456-041X","authenticated-orcid":false,"given":"TORSTEN","family":"SCHAUB","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,9,21]]},"reference":[{"key":"S1471068420000344_ref7","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1016\/j.artint.2010.04.011","article-title":"Stable models and circumscription","volume":"1","author":"Ferraris","year":"2011","journal-title":"Artificial Intelligence 175"},{"key":"S1471068420000344_ref18","unstructured":"18. Lifschitz, V. , L\u00fchne, P. , and Schaub, T. 2020. Towards verifying logic programs in the input language of CLINGO. In Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday, Springer, 190\u2013209."},{"key":"S1471068420000344_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068417000394"},{"key":"S1471068420000344_ref12","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/j.artint.2017.02.002","article-title":"Infinitary equilibrium logic and strongly equivalent logic programs","author":"Harrison","year":"2017","journal-title":"Artificial Intelligence 246"},{"key":"S1471068420000344_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001765"},{"key":"S1471068420000344_ref8","unstructured":"8. Ferraris, P. , Lee, J. , Lifschitz, V. , and Palla, R. 2009. Symmetric splitting in the general theory of stable models. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, AAAI\/MIT Press, 797\u2013803."},{"key":"S1471068420000344_ref15","unstructured":"15. Lee, J. , Lifschitz, V. , and Palla, R. 2008. A reductive semantics for counting and choice in answer set programming. In Proceedings of the 23rd National Conference on Artificial Intelligence, AAAI Press, 472\u2013479."},{"key":"S1471068420000344_ref6","unstructured":"6. Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning, Springer, 119\u2013131."},{"key":"S1471068420000344_ref3","unstructured":"3. Clark, K. 1978. Negation as failure. In Logic and Data Bases, Plenum Press, 293\u2013322."},{"key":"S1471068420000344_ref17","unstructured":"17. Lifschitz, V. , L\u00fchne, P. , and Schaub, T. 2019. Verifying strong equivalence of programs in the input language of GRINGO. In Proceedings of the 15th International Conference and Symposium of Logic Programming and Nonmonotonic Reasoning, Springer, 270\u2013283."},{"key":"S1471068420000344_ref1","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/2043174.2043195","article-title":"Answer set programming at a glance","volume":"12","author":"Brewka","year":"2011","journal-title":"Communications of the ACM 54"},{"key":"S1471068420000344_ref16","unstructured":"16. Lifschitz, V. , L\u00fchne, P. , and Schaub, T. 2018. anthem: Transforming gringo programs into first-order theories (preliminary report). In Proceedings of the 11th Workshop on Answer Set Programming and Other Computing Paradigms,"},{"key":"S1471068420000344_ref10","unstructured":"10. Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the 5th International Conference on Logic Programming, MIT Press, 1070\u20131080."},{"key":"S1471068420000344_ref14","unstructured":"14. Kov\u00e1cs, L. and Voronkov, A. 2013. First-order theorem proving and Vampire. In Proceedings of the 25th International Conference on Computer Aided Verification, Springer, 1\u201335."},{"key":"S1471068420000344_ref21","unstructured":"21. Truszczy\u0144ski, M. 2012. Connecting first-order ASP and the logic FO(ID) through reducts. In Correct Reasoning: Essays on Logic-Based AI in Honour of Vladimir Lifschitz, Springer, 543\u2013559."},{"key":"S1471068420000344_ref19","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1093\/logcom\/exn039","article-title":"A translation-based approach to the verification of modular equivalence","volume":"4","author":"Oikarinen","year":"2009","journal-title":"Journal of Logic and Computation 19"},{"key":"S1471068420000344_ref9","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1017\/S1471068415000150","article-title":"Abstract Gringo","volume":"4","author":"Gebser","year":"2015","journal-title":"Theory and Practice of Logic Programming 15"},{"key":"S1471068420000344_ref20","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP problem library and associated infrastructure","volume":"4","author":"Sutcliffe","year":"2017","journal-title":"Journal of Automated Reasoning 59"},{"key":"S1471068420000344_ref11","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1142\/S0218194096000053","article-title":"Towards a theory of elaboration tolerance: Logic programming approach","volume":"1","author":"Gelfond","year":"1996","journal-title":"International Journal of Software Engineering and Knowledge Engineering 6"},{"key":"S1471068420000344_ref2","doi-asserted-by":"crossref","unstructured":"2. Cabalar, P. , Fandinno, J. , and Lierler, Y. 2020. Modular answer set programming as a formal specification language. Theory and Practice of Logic Programming, this volume.","DOI":"10.1017\/S1471068420000265"},{"key":"S1471068420000344_ref5","first-page":"51","article-title":"Consistency of Clark\u2019s completion and the existence of stable models","author":"Fages","year":"1994","journal-title":"Journal of Methods of Logic in Computer Science 1"}],"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\/S1471068420000344","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,14]],"date-time":"2021-01-14T08:49:42Z","timestamp":1610614182000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068420000344\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9]]},"references-count":21,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,9]]}},"alternative-id":["S1471068420000344"],"URL":"https:\/\/doi.org\/10.1017\/s1471068420000344","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}