{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T11:32:46Z","timestamp":1676892766898},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2008,11,1]],"date-time":"2008-11-01T00:00:00Z","timestamp":1225497600000},"content-version":"unspecified","delay-in-days":0,"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":[[2008,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce an extended tableau calculus for answer set programming (ASP). The\n                    proof system is based on the ASP tableaux defined in the work by Gebser and\n                    Schaub (Tableau calculi for answer set programming. In <jats:italic>Proceedings of\n                        the 22nd International Conference on Logic Programming (ICLP 2006)<\/jats:italic>,\n                    S. Etalle and M. Truszczynski, Eds. Lecture Notes in Computer Science, vol.\n                    4079. Springer, 11\u201325) with an added extension rule. We investigate\n                    the power of Extended ASP Tableaux both theoretically and empirically. We study\n                    the relationship of Extended ASP Tableaux with the Extended Resolution proof\n                    system defined by Tseitin for sets of clauses, and separate Extended ASP\n                    Tableaux from ASP Tableaux by giving a polynomial-length proof for a family of\n                    normal logic programs {\u03a6<jats:sub><jats:italic>n<\/jats:italic><\/jats:sub>} for which ASP Tableaux has exponential-length minimal proofs with\n                    respect to <jats:italic>n<\/jats:italic>. Additionally, Extended ASP Tableaux imply\n                    interesting insight into the effect of program simplification on the lengths of\n                    proofs in ASP. Closely related to Extended ASP Tableaux, we empirically\n                    investigate the effect of redundant rules on the efficiency of ASP solving.<\/jats:p>","DOI":"10.1017\/s1471068408003578","type":"journal-article","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T03:40:37Z","timestamp":1224214837000},"page":"691-716","source":"Crossref","is-referenced-by-count":5,"title":["Extended ASP Tableaux and rule redundancy in normal logic\n                        programs"],"prefix":"10.1017","volume":"8","author":[{"given":"MATTI","family":"J\u00c4RVISALO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"EMILIA","family":"OIKARINEN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2008,11,1]]},"reference":[{"key":"S1471068408003578_ref43","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part\n                    II","author":"Tseitin","year":"1969"},{"key":"S1471068408003578_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45241-9_12"},{"key":"S1471068408003578_ref39","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"S1471068408003578_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"S1471068408003578_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.04.004"},{"key":"S1471068408003578_ref35","first-page":"853","volume-title":"Proceedings of the 18th\n                        International Joint Conference on Artificial Intelligence (IJCAI\n                    2003)","author":"Lin","year":"2003"},{"key":"S1471068408003578_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1131313.1131316"},{"key":"S1471068408003578_ref30","first-page":"134","volume-title":"Proceedings of the 23rd International Conference on Logic\n                        Programming (ICLP 2007)","author":"J\u00e4rvisalo","year":"2007"},{"key":"S1471068408003578_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S1471068408003578_ref25","first-page":"37","volume-title":"Proceedings of the 21st International\n                        Conference on Logic Programming (ICLP 2005)","author":"Giunchiglia","year":"2005"},{"key":"S1471068408003578_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9033-2"},{"key":"S1471068408003578_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00207-2"},{"key":"S1471068408003578_ref21","first-page":"119","volume-title":"Proceedings of the 23rd International Conference on Logic\n                        Programming (ICLP 2007)","author":"Gebser","year":"2007"},{"key":"S1471068408003578_ref20","first-page":"11","volume-title":"Proceedings of the 22nd International Conference on Logic\n                        Programming (ICLP 2006)","author":"Gebser","year":"2006"},{"key":"S1471068408003578_ref26","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027339205632"},{"key":"S1471068408003578_ref4","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","article-title":"Towards understanding and harnessing the\n                        potential of clause learning","volume":"22","author":"Beame","year":"2004","journal-title":"Journal of Artificial\n                        Intelligence Research"},{"key":"S1471068408003578_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1149114.1149117"},{"key":"S1471068408003578_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00187-X"},{"key":"S1471068408003578_ref12","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"S1471068408003578_ref29","unstructured":"J\u00e4rvisalo M. and Junttila T. in press. Limitations of restricted branching in clause learning. Constraints."},{"key":"S1471068408003578_ref34","first-page":"23","volume-title":"Proceedings of the 11th\n                        International Conference on Logic Programming","author":"Lifschitz","year":"1994"},{"key":"S1471068408003578_ref28","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.16.35-86"},{"key":"S1471068408003578_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_8"},{"key":"S1471068408003578_ref38","first-page":"530","volume-title":"Proceedings of the 38th Design Automation Conference (DAC\n                    2001)","author":"Moskewicz","year":"2001"},{"key":"S1471068408003578_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002729"},{"key":"S1471068408003578_ref42","unstructured":"Soininen T. , Niemel\u00e4 I. , Tiihonen J. and Sulonen R. 2001. Representing configuration knowledge with weight constraint rules. In Proceedings of the 1st International Workshop on Answer Set Programming: Towards Efficient and Scalable Knowledge (ASP 2001), Provetti A. and Son T. C. , Eds."},{"key":"S1471068408003578_ref1","first-page":"769","volume-title":"Proceedings of the\n                        17th European Conference on Artificial Intelligence (ECAI 2006)","author":"Anger","year":"2006"},{"key":"S1471068408003578_ref19","first-page":"41","volume-title":"ICLP Workshop on Search and Logic: Answer Set Programming and\n                    SAT","author":"Gebser","year":"2006"},{"key":"S1471068408003578_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59487-6_7"},{"key":"S1471068408003578_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BF01530761"},{"key":"S1471068408003578_ref17","first-page":"51","article-title":"Consistency of Clark's completion and\n                        existence of stable models","volume":"1","author":"Fages","year":"1994","journal-title":"Journal of Methods of\n                        Logic in Computer Science"},{"key":"S1471068408003578_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00186-8"},{"key":"S1471068408003578_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1008335.1008338"},{"key":"S1471068408003578_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"S1471068408003578_ref15","first-page":"87","volume-title":"Proceedings of the 7th International Conference on Logic\n                        Programming and Nonmonotonic Reasoning (LPNMR 2004)","author":"Eiter","year":"2004"},{"key":"S1471068408003578_ref23","first-page":"1070","volume-title":"Proceedings of the 5th International Conference and Symposium on\n                        Logic Programming (ICLP\/SLP 1988)","author":"Gelfond","year":"1988"},{"key":"S1471068408003578_ref18","first-page":"286","volume-title":"Proceedings of\n                        the 20th International Joint Conference on Articifial Intelligence (IJCAI\n                        2007)","author":"Gebser","year":"2007"},{"key":"S1471068408003578_ref5","first-page":"66","article-title":"Propositional proof complexity: Past, present,\n                        and future","volume":"65","author":"Beame","year":"1998","journal-title":"Bulletin of the EATCS"},{"key":"S1471068408003578_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543357"},{"key":"S1471068408003578_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"S1471068408003578_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9082-1"},{"key":"S1471068408003578_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068408003578_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"}],"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\/S1471068408003578","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T15:36:57Z","timestamp":1554046617000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068408003578\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11]]},"references-count":43,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2008,11]]}},"alternative-id":["S1471068408003578"],"URL":"https:\/\/doi.org\/10.1017\/s1471068408003578","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11]]}}}