{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T21:01:21Z","timestamp":1750453281993},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439295"},{"type":"electronic","value":"9783540456162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_8","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:26:55Z","timestamp":1179376015000},"page":"100-114","source":"Crossref","is-referenced-by-count":5,"title":["Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Eiter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Volker","family":"Klotz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Tompits","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Woltran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"P. Bonatti and N. Olivetti. Sequent Calculi for Propositional Nonmonotonic Logics. ACM Transactions on Computational Logic, 2002. To appear.","DOI":"10.1145\/505372.505374"},{"key":"8_CR2","unstructured":"G. Brewka. Tweety-Still Flying: Some Remarks on Abnormal Birds, Applicable Rules and a Default Prover. In Proc. AAAI-86, pages 8\u201312, 1986."},{"key":"8_CR3","unstructured":"G. Brewka. Nonmonotonic Reasoning: Logical Foundations of Commonsense. Cambridge University Press, 1991."},{"key":"8_CR4","unstructured":"G. Brewka and K. Wittur. Nichtmonotone Logiken. Universit\u00e4t Bonn, Informatik Berichte 40, 1984."},{"key":"8_CR5","unstructured":"M. Cadoli, A. Giovanardi, and M. Schaerf. An Algorithm to Evaluate Quantified Boolean Formulae. In Proc. AAAI-98, pages 262\u2013267, 1998."},{"key":"8_CR6","unstructured":"P. Cholewinski, W. Marek, and M. Truszcy\u0144ski. Default Reasoning System DeReS. In Proc. KR-96, pages 518\u2013528, 1996."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"J. Delgrande, T. Schaub, H. Tompits, and S. Woltran. On Computing Solutions to Belief Change Scenarios. In Proc. ECSQARU-01, pages 510\u2013521, 2001.","DOI":"10.1007\/3-540-44652-4_45"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"E. Eder. Relative Complexities of First-Order Calculi. Vieweg Verlag, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1006\/jsco.1996.0044","volume":"22","author":"U. Egly","year":"1996","unstructured":"U. Egly. On Different Structure-preserving Translations to Normal Form. Journal of Symbolic Computation, 22:121\u2013142, 1996.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR10","unstructured":"U. Egly, T. Eiter, V. Klotz, H. Tompits, and S. Woltran. Computing Stable Models with Quantified Boolean Formulas: Some Experimental Results. In Proc. AAAI Spring Symposium-01, pages 53\u201359, 2001."},{"key":"8_CR11","unstructured":"U. Egly, T. Eiter, H. Tompits, and S. Woltran. Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In Proc. AAAI-00, pages 417\u2013422, 2000."},{"key":"8_CR12","unstructured":"U. Egly, V. Klotz, H. Tompits, and S. Woltran. A Toolbox for Abduction: Preliminary Report. In Proc. IJCAR-Workshop on Theory and Applications of Quantified Boolean Formulas, pages 29\u201339, 2001."},{"issue":"1\u20132","key":"8_CR13","doi-asserted-by":"crossref","first-page":"31","DOI":"10.3233\/FI-1992-171-204","volume":"17","author":"T. Eiter","year":"1992","unstructured":"T. Eiter and G. Gottlob. Complexity of Reasoning with Parsimonious and Moderately Grounded Expansions. Fundamenta Informaticae, 17(1\u20132):31\u201353, 1992.","journal-title":"Fundamenta Informaticae"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"T. Eiter, N. Leone, C. Mateis, G. Pfeifer, and F. Scarcello. A Deductive System for Nonmonotonic Reasoning. In Proc. LPNMR-97, pages 363\u2013374, 1997.","DOI":"10.1007\/3-540-63255-7_27"},{"key":"8_CR15","unstructured":"R. Feldmann, B. Monien, and S. Schamberger. A Distributed Algorithm to Evaluate Quantified Boolean Formulas. In Proc. AAAI-00, pages 285\u2013290, 2000."},{"key":"8_CR16","unstructured":"M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In Proc. ICLP-88, pages 1070\u20131080, 1988."},{"key":"8_CR17","unstructured":"I. P. Gent and T. Walsh. Beyond NP: The QSAT Phase Transition. In Proc. AAAI-99, pages 648\u2013653, 1999."},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Narizzano, and A. Tacchella. QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In Proc. IJCAR-01, pages 364\u2013369, 2001.","DOI":"10.1007\/3-540-45744-5_27"},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1093\/logcom\/2.3.397","volume":"2","author":"G. Gottlob","year":"1992","unstructured":"G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2(3):397\u2013425, 1992.","journal-title":"Journal of Logic and Computation"},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1145\/210332.210334","volume":"42","author":"G. Gottlob","year":"1995","unstructured":"G. Gottlob. Translating Default Logic into Standard Autoepistemic Logic. Journal of the ACM, 42(4):711\u2013740, 1995.","journal-title":"Journal of the ACM"},{"key":"8_CR21","unstructured":"U. Junker and K. Konolige. Computing the Extensions of Autoepistemic and Default Logic with a TMS. In Proc. AAAI-90, pages 278\u2013283, 1990."},{"key":"8_CR22","unstructured":"H. Kautz and B. Selman. Planning as Satisfiability. In Proc. ECAI-92, pages 359\u2013363, 1992."},{"issue":"1","key":"8_CR23","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine-B\u00fcning","year":"1995","unstructured":"H. Kleine-B\u00fcning, M. Karpinski, and A. Fl\u00f6gel. Resolution for Quantified Boolean Formulas. Information and Computation, 117(1):12\u201318, 1995.","journal-title":"Information and Computation"},{"issue":"3","key":"8_CR24","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0004-3702(88)90021-5","volume":"35","author":"K. Konolige","year":"1988","unstructured":"K. Konolige. On the Relation Between Default and Autoepistemic Logic. Artificial Intelligence, 35(3):343\u2013382, 1988.","journal-title":"Artificial Intelligence"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"R. Letz. Advances in Decision Procedures for Quantified Boolean Formulas. In Proc. IJCAR-Workshop on Theory and Applications of Quantified Boolean Formulas, pages 55\u201364, 2001.","DOI":"10.1007\/3-540-45616-3_12"},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF01531081","volume":"1","author":"W. Marek","year":"1990","unstructured":"W. Marek and M. Truszczy\u0144ski. Modal Logic for Default Reasoning. Annals of Mathematics and Artificial Intelligence, 1:275\u2013302, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"F. Massacci. Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison. In Proc. TABLEAUX-99, pages 14\u201318, 1999.","DOI":"10.1007\/3-540-48754-9_2"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J. McCarthy","year":"1980","unstructured":"J. McCarthy. Circumscription-A Form of Nonmonotonic Reasoning. Artificial Intelligence, 13:27\u201339, 1980.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"8_CR29","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0004-3702(85)90042-6","volume":"25","author":"R. C. Moore","year":"1985","unstructured":"R. C. Moore. Semantical Considerations on Nonmonotonic Logic. Artificial Intelligence, 25(1):75\u201394, 1985.","journal-title":"Artificial Intelligence"},{"key":"8_CR30","doi-asserted-by":"crossref","first-page":"117","DOI":"10.3233\/FI-1992-171-208","volume":"17","author":"I. Niemel\u00e4","year":"1992","unstructured":"I. Niemel\u00e4. On the Decidability and Complexity of Autoepistemic Reasoning. Fundamenta Informaticae, 17:117\u2013155, 1992.","journal-title":"Fundamenta Informaticae"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"I. Niemel\u00e4 and P. Simons. Smodels: An Implementation of the Stable Model and Well-Founded Semantics for Normal Logic Programs. In Proc. LPNMR-97, pages 420\u2013429, 1997.","DOI":"10.1007\/3-540-63255-7_32"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"D. Pearce, H. Tompits, and S. Woltran. Encodings for Equilibrium Logic and Logic Programs with Nested Expressions. In Proc. EPIA-01, pages 306\u2013320. Springer, 2001.","DOI":"10.1007\/3-540-45329-6_31"},{"issue":"3","key":"8_CR33","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum. A Structure Preserving Clause Form Translation. Journal of Symbolic Computation, 2(3):293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR34","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BF03037171","volume":"9","author":"T. Przymusinski","year":"1991","unstructured":"T. Przymusinski. Stable Semantics for Disjunctive Programs. New Generation Computing Journal, 9:401\u2013424, 1991.","journal-title":"New Generation Computing Journal"},{"issue":"1\u20132","key":"8_CR35","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","volume":"13","author":"R. Reiter","year":"1980","unstructured":"R. Reiter. A Logic for Default Reasoning. Artificial Intelligence, 13(1\u20132):81\u2013132, Apr. 1980.","journal-title":"Artificial Intelligence"},{"key":"8_CR36","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"J. Rintanen. Constructing Conditional Plans by a Theorem Prover. Journal of Artificial Intelligence Research, 10:323\u2013352, 1999.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"8_CR37","unstructured":"J. Rintanen. Improvements to the Evaluation of Quantified Boolean Formulae. In Proc. IJCAI-99, pages 1192\u20131197, 1999."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45616-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:04:33Z","timestamp":1683842673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}