{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,29]],"date-time":"2026-06-29T14:02:30Z","timestamp":1782741750508,"version":"3.54.5"},"reference-count":28,"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>In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a <jats:italic>formal proof<\/jats:italic> showing that the answer sets of a given (non-ground) logic program <jats:italic>P<\/jats:italic> correctly correspond to the solutions to the problem encoded by <jats:italic>P<\/jats:italic>, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) <jats:italic>program modules<\/jats:italic> that may incorporate local hidden atoms at different levels. Then, <jats:italic>verifying<\/jats:italic> the logic program <jats:italic>P<\/jats:italic> amounts to prove some kind of equivalence between <jats:italic>P<\/jats:italic> and its modular specification.<\/jats:p>","DOI":"10.1017\/s1471068420000265","type":"journal-article","created":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T05:25:42Z","timestamp":1600665942000},"page":"767-782","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":12,"title":["Modular Answer Set Programming as a Formal Specification Language"],"prefix":"10.1017","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7440-0953","authenticated-orcid":false,"given":"PEDRO","family":"CABALAR","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3917-8717","authenticated-orcid":false,"given":"JORGE","family":"FANDINNO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6146-623X","authenticated-orcid":false,"given":"YULIYA","family":"LIERLER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,9,21]]},"reference":[{"key":"S1471068420000265_ref28","unstructured":"28. Pearce, D. and Valverde, A. 2008. Quantified equilibrium logic and foundations for answer set programs. In Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings, de la Banda, M. G. and Pontelli, E. , Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 546\u2013560."},{"key":"S1471068420000265_ref16","doi-asserted-by":"crossref","unstructured":"16. Lierler, Y. 2019. Strong equivalence and program\u2019s structure in arguing essential equivalence between first-order logic programs. In Proceedings of the 21st International Symposium on Practical Aspects of Declarative Languages (PADL).","DOI":"10.1007\/978-3-030-05998-9_1"},{"key":"S1471068420000265_ref27","unstructured":"27. Pearce, D. and Valverde, A. 2004. Synonymous theories in answer set programming and equilibrium logic. In Proceedings of the 16th European Conference on Artificial Intelligence. ECAI\u201904. IOS Press, Amsterdam, The Netherlands, The Netherlands, 388\u2013392."},{"key":"S1471068420000265_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.07.005"},{"key":"S1471068420000265_ref3","doi-asserted-by":"crossref","unstructured":"3. Buddenhagen, M. and Lierler, Y. 2015. Performance tuning in answer set programming. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR).","DOI":"10.1007\/978-3-319-23264-5_17"},{"key":"S1471068420000265_ref20","doi-asserted-by":"crossref","unstructured":"20. Lifschitz, V. , Pearce, D. , and Valverde, A. 2007. A characterization of strong equivalence for logic programs with variables. In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 188\u2013200.","DOI":"10.1007\/978-3-540-72200-7_17"},{"key":"S1471068420000265_ref14","unstructured":"14. Gon\u00e7alves, R. , Knorr, M. , and Leite, J. 2016. You can\u2019t always forget what you want: On the limits of forgetting in answer set programming. In Proceedings of 22nd European Conference on Artificial Intelligence (ECAI\u201916). Frontiers in Artificial Intelligence and Applications, vol. 285. IOS Press, 957\u2013965."},{"key":"S1471068420000265_ref12","unstructured":"12. Geibinger, T. and Tompits, H. 2019. Characterising relativised strong equivalence with projection for non-ground answer-set programs. In Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11468. Springer, 542\u2013558."},{"key":"S1471068420000265_ref21","unstructured":"21. Lifschitz, V. and Turner, H. 1994. Splitting a logic program. In Proceedings of the Eleventh International Conference on Logic Programming. MIT Press, 23\u201337."},{"key":"S1471068420000265_ref13","unstructured":"13. Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the Fifth International Conference and Symposium of Logic Programming (ICLP\u201988), Kowalski, R. and Bowen, K. , Eds. MIT Press, 1070\u20131080."},{"key":"S1471068420000265_ref17","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1017\/S1471068417000345","article-title":"Achievements in answer set programming","volume":"5","author":"Lifschitz","year":"2017","journal-title":"Theory and Practice of Logic Programming 17"},{"key":"S1471068420000265_ref18","unstructured":"18. Lifschitz, V. , L\u00fchne, P. , and Schaub, T. 2018. anthem: Transforming gringo programs into first-order theories (preliminary report). CoRR abs\/1810.00453."},{"key":"S1471068420000265_ref7","unstructured":"7. Erdo\u011fan, S. T. and Lifschitz, V. 2004. Definitions in answer set programming. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer-Verlag, 114\u2013126."},{"key":"S1471068420000265_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068420000265"},{"key":"S1471068420000265_ref6","unstructured":"6. Eiter, T. , Tompits, H. , and Woltran, S. 2005. On solution correspondences in answer set programming. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI\u201905), Kaelbling, L. and Saffiotti, A. , Eds. Professional Book Center, 97\u2013102."},{"key":"S1471068420000265_ref19","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1145\/383779.383783","article-title":"Strongly equivalent logic programs","volume":"4","author":"Lifschitz","year":"2001","journal-title":"ACM Transactions on Computational Logic 2"},{"key":"S1471068420000265_ref25","unstructured":"25. Oetsch, J. and Tompits, H. 2008. Program correspondence under the answer-set semantics: The non-ground case. In Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings, de la Banda, M. G. and Pontelli, E. , Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 591\u2013605."},{"key":"S1471068420000265_ref9","first-page":"25","article-title":"Logic programs with propositional connectives and aggregates","volume":"4","author":"Ferraris","year":"2011","journal-title":"ACM Transactions on Computational Logic 12"},{"key":"S1471068420000265_ref22","volume-title":"Paradigm: a","author":"Marek","year":"1999"},{"key":"S1471068420000265_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.04.011"},{"key":"S1471068420000265_ref8","doi-asserted-by":"crossref","unstructured":"8. Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 119\u2013131.","DOI":"10.1007\/11546207_10"},{"key":"S1471068420000265_ref26","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":"J. Log. Comput. 19"},{"key":"S1471068420000265_ref5","unstructured":"5. Denecker, M. , Lierler, Y. , Truszczy\u0144ski, M. , and Vennekens, J. 2012. A Tarskian informal semantics for answer set programming. In Technical Communications of the 28th International Conference on Logic Programming (ICLP). 277\u2013289."},{"key":"S1471068420000265_ref15","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/682"},{"key":"S1471068420000265_ref24","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"S1471068420000265_ref11","unstructured":"11. Gebser, M. , Kaufmann, B. , Neumann, A. , and Schaub, T. 2007. Conflict-driven answer set solving. In Proceedings of 20th International Joint Conference on Artificial Intelligence (IJCAI\u201907). MIT Press, 386\u2013392."},{"key":"S1471068420000265_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0043-0"},{"key":"S1471068420000265_ref2","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/2043174.2043195","article-title":"Answer set programming at a glance","author":"Brewka","year":"2011","journal-title":"Communications of the ACM 54(12)"}],"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\/S1471068420000265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,14]],"date-time":"2021-01-14T08:48:20Z","timestamp":1610614100000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068420000265\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9]]},"references-count":28,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,9]]}},"alternative-id":["S1471068420000265"],"URL":"https:\/\/doi.org\/10.1017\/s1471068420000265","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"}}]}}