{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:29:25Z","timestamp":1785202165941,"version":"3.55.0"},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T00:00:00Z","timestamp":1568937600000},"content-version":"unspecified","delay-in-days":19,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Answer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs.<\/jats:p>","DOI":"10.1017\/s1471068419000255","type":"journal-article","created":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T09:06:21Z","timestamp":1568970381000},"page":"891-907","source":"Crossref","is-referenced-by-count":5,"title":["Inconsistency Proofs for ASP: The ASP - DRUPE Format"],"prefix":"10.1017","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2052-2063","authenticated-orcid":false,"given":"MARIO","family":"ALVIANO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5617-5286","authenticated-orcid":false,"given":"CARMINE","family":"DODARO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JOHANNES K.","family":"FICHTE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0131-6771","authenticated-orcid":false,"given":"MARKUS","family":"HECHER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"TOBIAS","family":"PHILIPP","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JAKOB","family":"RATH","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2019,9,20]]},"reference":[{"key":"S1471068419000255_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043195"},{"key":"S1471068419000255_ref28","first-page":"91","volume-title":"IJCAR","volume":"8562","author":"Heule","year":"2014"},{"key":"S1471068419000255_ref40","unstructured":"Syrj\u00e4nen, T. 2000. Lparse 1.0 User\u2019s Manual."},{"key":"S1471068419000255_ref17","volume-title":"Synthesis Lectures on Artificial Intelligence and Machine Learning","author":"Gebser","year":"2012"},{"key":"S1471068419000255_ref15","first-page":"2:1","volume-title":"ICLP (Tech. C.)","volume":"52","author":"Gebser","year":"2016"},{"key":"S1471068419000255_ref26","first-page":"345","volume-title":"CADE 2013","volume":"7898","author":"Heule","year":"2013"},{"key":"S1471068419000255_ref13","first-page":"25:1","article-title":"Logic programs with propositional connectives and aggregates","volume":"4","author":"Ferraris","year":"2011","journal-title":"ACM Trans. Comput. Log. 12"},{"key":"S1471068419000255_ref21","unstructured":"Gelder, A. V. 2008. Verifying RUP proofs of propositional unsatisfiability. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008."},{"key":"S1471068419000255_ref14","first-page":"497","volume-title":"KR 2010","author":"Gebser","year":"2010"},{"key":"S1471068419000255_ref29","doi-asserted-by":"crossref","first-page":"35","DOI":"10.3166\/jancl.16.35-86","article-title":"Some (in)translatability results for normal logic programs and propositional theories","volume":"1","author":"Janhunen","year":"2006","journal-title":"Journal of Applied Non-Classical Logics 16"},{"key":"S1471068419000255_ref20","first-page":"323","article-title":"Detecting inconsistencies in large biological networks with answer set programming","volume":"2","author":"Gebser","year":"2011","journal-title":"TPLP 11"},{"key":"S1471068419000255_ref36","first-page":"415","volume-title":"JELIA 2016","volume":"10021","author":"Philipp","year":"2016"},{"key":"S1471068419000255_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s13218-018-0530-3"},{"key":"S1471068419000255_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10015-8"},{"key":"S1471068419000255_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.04.002"},{"key":"S1471068419000255_ref7","unstructured":"Clark, K. L. 1977. Negation as failure. In Symposium on Logic and Data Bases 1977. Advances in Data Base Theory. Plemum Press, 293\u2013322."},{"key":"S1471068419000255_ref4","doi-asserted-by":"crossref","first-page":"63","DOI":"10.3233\/FI-2016-1398","article-title":"Answer set programming modulo acyclicity","volume":"1","author":"Bomanson","year":"2016","journal-title":"Fundam. Inform. 147"},{"key":"S1471068419000255_ref1","first-page":"40","volume-title":"LPNMR 2015","volume":"9345","author":"Alviano","year":"2015"},{"key":"S1471068419000255_ref2","first-page":"301","article-title":"Shared aggregate sets in answer set programming","volume":"3","author":"Alviano","year":"2018","journal-title":"TPLP 18"},{"key":"S1471068419000255_ref3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/s10472-006-9026-1","article-title":"Answer set based design of knowledge systems","volume":"1","author":"Balduccini","year":"2006","journal-title":"Ann. Math. Artif. Intell. 47,"},{"key":"S1471068419000255_ref6","unstructured":"Calimeri, F. , Faber, W. , Gebser, M. , Ianni, G. , Kaminski, R. , Krennwallner, T. , Leone, N. , Ricca, F. , and Schaub, T. 2015. ASP-core-2 input language format."},{"key":"S1471068419000255_ref8","first-page":"220","volume-title":"CADE 2017","volume":"10395","author":"Cruz-Filipe","year":"2017"},{"key":"S1471068419000255_ref9","first-page":"61","volume-title":"SAT 2005","volume":"3569","author":"E\u00e9n","year":"2005"},{"key":"S1471068419000255_ref10","first-page":"40","volume-title":"LPNMR 2005","volume":"3662","author":"Faber","year":"2005"},{"key":"S1471068419000255_ref16","first-page":"1","volume-title":"ICLP 2011","volume":"11","author":"Gebser","year":"2011"},{"key":"S1471068419000255_ref19","doi-asserted-by":"crossref","unstructured":"Gebser, M. , Obermeier, P. , Ratsch-Heitmann, M. , Runge, M. , and Schaub, T. 2018. Routing driverless transport vehicles in car assembly with answer set programming. CoRR abs\/1804.10437.","DOI":"10.29007\/h1kk"},{"key":"S1471068419000255_ref23","unstructured":"Goldberg, E. I. and Novikov, Y. 2003. Verification of proofs of unsatisfiability for CNF formulas. In DATE. IEEE Computer Society, 10886\u201310891."},{"key":"S1471068419000255_ref24","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btt393"},{"key":"S1471068419000255_ref27","first-page":"591","volume-title":"CADE 2015","volume":"9195","author":"Heule","year":"2015"},{"key":"S1471068419000255_ref30","first-page":"516","volume-title":"IJCAR 2018","volume":"10900","author":"Kiesl","year":"2018"},{"key":"S1471068419000255_ref31","first-page":"853","volume-title":"IJCAI\u201903","author":"Lin","year":"2003"},{"key":"S1471068419000255_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2009.11.016"},{"key":"S1471068419000255_ref33","first-page":"161","volume-title":"IJCAR","volume":"10900","author":"Lonsing","year":"2018"},{"key":"S1471068419000255_ref35","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/S1471068406002973","article-title":"Well-founded and stable semantics of logic programs with aggregates","volume":"3","author":"Pelov","year":"2007","journal-title":"Theory and Practice of Logic Programming 7"},{"key":"S1471068419000255_ref37","unstructured":"Ricca, F. , Grasso, G. , Alviano, M. , Manna, M. , Lio, V. , Iiritano, S. , and Leone, N. 2012. Team-building with answer set programming in the Gioia-Tauro seaport. TPLP 12, 361\u2013381."},{"key":"S1471068419000255_ref38","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"S1471068419000255_ref39","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002936"},{"key":"S1471068419000255_ref41","unstructured":"Truszczy\u0144ski, M. 2011. Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs. TPLP 11, 881\u2013904."},{"key":"S1471068419000255_ref42","first-page":"422","volume-title":"SAT 2014","volume":"8561","author":"Wetzler","year":"2014"},{"key":"S1471068419000255_ref22","first-page":"587","article-title":"Vicious circle principle and logic programs with aggregates","volume":"4","author":"Gelfond","year":"2014","journal-title":"TPLP 14"},{"key":"S1471068419000255_ref18","first-page":"15","volume-title":"ECAI 2008. Frontiers in Artificial Intelligence and Applications","volume":"178","author":"Gebser","year":"2008"},{"key":"S1471068419000255_ref12","first-page":"51","article-title":"Consistency of clark\u2019s completion and existence of stable models","volume":"1","author":"Fages","year":"1994","journal-title":"Meth. of Logic in CS 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\/S1471068419000255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T04:38:50Z","timestamp":1571114330000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068419000255\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":42,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S1471068419000255"],"URL":"https:\/\/doi.org\/10.1017\/s1471068419000255","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}