{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:24Z","timestamp":1725490224874},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540746089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74610-2_10","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T02:33:31Z","timestamp":1187922811000},"page":"134-148","source":"Crossref","is-referenced-by-count":5,"title":["Extended ASP Tableaux and Rule Redundancy in Normal Logic Programs"],"prefix":"10.1007","author":[{"given":"Matti","family":"J\u00e4rvisalo","sequence":"first","affiliation":[]},{"given":"Emilia","family":"Oikarinen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"10_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0004-3702(02)00187-X","volume":"138","author":"P. Simons","year":"2002","unstructured":"Simons, P., Niemel\u00e4, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence\u00a0138(1-2), 181\u2013234 (2002)","journal-title":"Artificial Intelligence"},{"key":"10_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/11591191_8","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Anger","year":"2005","unstructured":"Anger, C., Gebser, M., Linke, T., Neumann, A., Schaub, T.: The nomore++ approach to answer set solving. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS(LNAI), vol.\u00a03835, pp. 95\u2013109. Springer, Heidelberg (2005)"},{"issue":"3","key":"10_CR3","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1145\/1149114.1149117","volume":"7","author":"N. Leone","year":"2006","unstructured":"Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. ACM TOCL\u00a07(3), 499\u2013562 (2006)","journal-title":"ACM TOCL"},{"key":"10_CR4","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: IJCAI, pp. 286\u2013392 (2007)"},{"key":"10_CR5","first-page":"66","volume":"65","author":"P. Beame","year":"1998","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: Past, present, and future. Bulletin of the EATCS\u00a065, 66\u201389 (1998)","journal-title":"Bulletin of the EATCS"},{"key":"10_CR6","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research\u00a022, 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/11799573_4","volume-title":"Logic Programming","author":"M. Gebser","year":"2006","unstructured":"Gebser, M., Schaub, T.: Tableau calculi for answer set programming. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol.\u00a04079, pp. 11\u201325. Springer, Heidelberg (2006)"},{"key":"10_CR8","first-page":"769","volume-title":"ECAI","author":"C. Anger","year":"2006","unstructured":"Anger, C., Gebser, M., Janhunen, T., Schaub, T.: What\u2019s a head without a body? In: ECAI, pp. 769\u2013770. IOS Press, Amsterdam (2006)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11562931_6","volume-title":"Logic Programming","author":"E. Giunchiglia","year":"2005","unstructured":"Giunchiglia, E., Maratea, M.: On the relation between answer set and SAT procedures (or, between cmodels and smodels). In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 37\u201351. Springer, Heidelberg (2005)"},{"key":"10_CR10","unstructured":"Gebser, M., Schaub, T.: Characterizing ASP inferences by unit propagation. In: LaSh ICLP Workshop, pp. 41\u201356 (2006)"},{"key":"10_CR11","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic","author":"G. Tseitin","year":"1983","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning 2: Classical Papers on Computational Logic, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"10_CR12","first-page":"1070","volume-title":"ICLP","author":"M. Gelfond","year":"1988","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: ICLP, pp. 1070\u20131080. MIT Press, Cambridge (1988)"},{"issue":"3-4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I. Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence\u00a025(3-4), 241\u2013273 (1999)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"2","key":"10_CR14","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1145\/1131313.1131316","volume":"7","author":"V. Lifschitz","year":"2006","unstructured":"Lifschitz, V., Razborov, A.: Why are there so many loop formulas? ACM Transactions on Computational Logic\u00a07(2), 261\u2013268 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1-2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01530761","volume":"12","author":"R. Ben-Eliyahu","year":"1994","unstructured":"Ben-Eliyahu, R., Dechter, R.: Propositional semantics for disjunctive logic programs. Annals of Mathematics and Artificial Intelligence\u00a012(1-2), 53\u201387 (1994)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1-2","key":"10_CR16","doi-asserted-by":"publisher","first-page":"35","DOI":"10.3166\/jancl.16.35-86","volume":"16","author":"T. Janhunen","year":"2006","unstructured":"Janhunen, T.: Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics\u00a016(1-2), 35\u201386 (2006)","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"1\u20132","key":"10_CR17","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.artint.2004.04.004","volume":"157","author":"F. Lin","year":"2004","unstructured":"Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence\u00a0157(1\u20132), 115\u2013137 (2004)","journal-title":"Artificial Intelligence"},{"issue":"4","key":"10_CR18","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s10817-006-9033-2","volume":"36","author":"E. Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Lierler, Y., Maratea, M.: Answer set programming based on propositional satisfiability. Journal of Automated Reasoning\u00a036(4), 345\u2013377 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR19","first-page":"311","volume-title":"Readings in nonmonotonic reasoning","author":"K. Clark","year":"1987","unstructured":"Clark, K.: Negation as failure. In: Readings in nonmonotonic reasoning, pp. 311\u2013325. Morgan Kaufmann Publishers, San Francisco (1987)"},{"key":"10_CR20","first-page":"51","volume":"1","author":"F. Fages","year":"1994","unstructured":"Fages, F.: Consistency of Clark\u2019s completion and existence of stable models. Journal of Methods of Logic in Computer Science\u00a01, 51\u201360 (1994)","journal-title":"Journal of Methods of Logic in Computer Science"},{"issue":"4","key":"10_CR21","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/s00493-004-0036-5","volume":"24","author":"E. Ben-Sasson","year":"2004","unstructured":"Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of tree-like and general resolution. Combinatorica\u00a024(4), 585\u2013603 (2004)","journal-title":"Combinatorica"},{"issue":"7","key":"10_CR22","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"4","key":"10_CR23","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"S.A. Cook","year":"1976","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News\u00a08(4), 28\u201332 (1976)","journal-title":"SIGACT News"},{"issue":"2-3","key":"10_CR24","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. TCS\u00a039(2-3), 297\u2013308 (1985)","journal-title":"TCS"},{"key":"10_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-24609-1_10","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"T. Eiter","year":"2003","unstructured":"Eiter, T., Fink, M., Tompits, H., Woltran, S.: Simplifying logic programs under uniform and strong equivalence. In: Lifschitz, V., Niemel\u00e4, I. (eds.) Logic Programming and Nonmonotonic Reasoning. LNCS (LNAI), vol.\u00a02923, pp. 87\u201399. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74610-2_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:29:58Z","timestamp":1619519398000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74610-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540746089"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74610-2_10","relation":{},"subject":[]}}