{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:53Z","timestamp":1747592453324},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_21","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"260-274","source":"Crossref","is-referenced-by-count":8,"title":["A New Clausal Class Decidable by Hyperresolution"],"prefix":"10.1007","author":[{"given":"Lilia","family":"Georgieva","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"issue":"5","key":"21_CR1","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1093\/jigpal\/3.5.685","volume":"3","author":"H. Andr\u00e9ka","year":"1995","unstructured":"H. Andr\u00e9ka, J. van Benthem, and I. N\u00e9meti. Back and forth between modal logic and classical logic. Bull. IGPL, 3(5):685\u2013720, 1995.","journal-title":"Bull. IGPL"},{"issue":"2","key":"21_CR2","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1006\/jsco.1999.0358","volume":"29","author":"C. Aravindan","year":"2000","unstructured":"C. Aravindan and P. Baumgartner. Theorem proving techniques for view deletion in databases. J. Symbolic Computat., 29(2):119\u2013147, 2000.","journal-title":"J. Symbolic Computat."},{"doi-asserted-by":"crossref","unstructured":"M. Baaz, U. Egly, and A. Leitsch. Normal form transformations. In Handbook of Automated Reasoning, pp. 273\u2013333. Elsevier, 2001.","key":"21_CR3","DOI":"10.1016\/B978-044450813-3\/50007-2"},{"doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Resolution theorem proving. In Handbook of Automated Reasoning, pp. 19\u201399. Elsevier, 2001.","key":"21_CR4","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"21_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Proc. KGC\u201993","author":"L. Bachmair","year":"1993","unstructured":"L. Bachmair, H. Ganzinger, and U. Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Proc. KGC\u201993, vol. 713 of LNCS, pp. 83\u201396. Springer, 1993."},{"unstructured":"P. Baumgartner, P. Fr\u00f6hlich, U. Furbach, and W. Nejdl. Semantically guided theorem proving for diagnosis applications. In Proc. IJCAI\u201997, pp. 460\u2013465. Morgan Kaufmann, 1997.","key":"21_CR6"},{"doi-asserted-by":"crossref","unstructured":"P. Baumgartner, J. Horton, and B. Spencer. Merge path improvements for minimal model hyper tableaux. In Proc. TABLEAUX\u201999, vol. 1617 of LNAI. Springer, 1999.","key":"21_CR7","DOI":"10.1007\/3-540-48754-9_9"},{"issue":"1","key":"21_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F. Bry","year":"2000","unstructured":"F. Bry and A. Yahya. Positive unit hyperresolution tableaux for minimal model generation. J. Automated Reasoning, 25(1):35\u201382, 2000.","journal-title":"J. Automated Reasoning"},{"unstructured":"H. de Nivelle. Translation of S4 into GF and 2VAR. Manuscript, 1999.","key":"21_CR9"},{"issue":"3","key":"21_CR10","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H. Nivelle de","year":"2000","unstructured":"H. de Nivelle, R. A. Schmidt, and U. Hustadt. Resolution-based methods for modal logics. Logic J. IGPL, 8(3):265\u2013292, 2000.","journal-title":"Logic J. IGPL"},{"unstructured":"C. G. Ferm\u00fcller, A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures. In Handbook of Automated Reasoning, pp. 1791\u20131849. Elsevier, 2001.","key":"21_CR11"},{"doi-asserted-by":"crossref","unstructured":"H. Ganzinger and H. de Nivelle. A superposition decision procedure for the guarded fragment with equality. In Proc. LICS\u201999, pp. 295\u2013303. IEEE Computer Society Press, 1999.","key":"21_CR12","DOI":"10.1109\/LICS.1999.782624"},{"unstructured":"L. Georgieva, U. Hustadt, and R. A. Schmidt. Hyperresolution for guarded formulae. To appear in J. Symbolic Computat.","key":"21_CR13"},{"doi-asserted-by":"crossref","unstructured":"L. Georgieva, U. Hustadt, and R. A. Schmidt. Computational space efficiency and minimal model generation for guarded formulae. In Proc. LPAR 2001, vol. 2250 of LNAI, pp. 85\u201399. Springer, 2001.","key":"21_CR14","DOI":"10.1007\/3-540-45653-8_6"},{"key":"21_CR15","doi-asserted-by":"publisher","first-page":"1719","DOI":"10.2307\/2586808","volume":"64","author":"E. Gr\u00e4del","year":"1999","unstructured":"E. Gr\u00e4del. On the restraining power of guards. J. Symbolic Logic, 64:1719\u20131742, 1999.","journal-title":"J. Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"U. Hustadt and R. A. Schmidt. Maslov\u2019s class K revisited. In Proc. CADE-16, vol. 1632 of LNAI, pp. 172\u2013186. Springer, 1999.","key":"21_CR16","DOI":"10.1007\/3-540-48660-7_12"},{"doi-asserted-by":"crossref","unstructured":"U. Hustadt and R. A. Schmidt. Issues of decidability for description logics in the framework of resolution. In Automated Deduction in Classical and Non-Classical Logics, vol. 1761 of LNAI, pp. 191\u2013205. Springer, 2000.","key":"21_CR17","DOI":"10.1007\/3-540-46508-1_13"},{"key":"21_CR18","first-page":"459","volume-title":"SAT 2000: Highlights of Satisfiability Research in the Year 2000","author":"U. Hustadt","year":"2000","unstructured":"U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. In SAT 2000: Highlights of Satisfiability Research in the Year 2000, pp. 459\u2013483. IOS Press, Amsterdam, 2000."},{"key":"21_CR19","doi-asserted-by":"crossref","first-page":"163","DOI":"10.3233\/FI-1993-182-406","volume":"18","author":"A. Leitsch","year":"1993","unstructured":"A. Leitsch. Deciding clause classes by semantic clash resolution. Fundamenta Informaticae, 18:163\u2013182, 1993.","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"crossref","unstructured":"C. Lutz. Complexity of terminological reasoning revisited. In Proc. LPAR\u201999, vol. 1705 of LNAI, pp. 181\u2013200. Springer, 1999.","key":"21_CR20","DOI":"10.1007\/3-540-48242-3_12"},{"unstructured":"C. Lutz, U. Sattler, and S. Tobies. A suggestion of an n-ary description logic. In Proc. DL\u201999, pp. 81\u201385. Link\u00f6ping University, 1999.","key":"21_CR21"},{"doi-asserted-by":"crossref","unstructured":"I. Niemel\u00e4. A tableau calculus for minimal model reasoning. In Proc. TABLEAUX\u201996, vol. 1071 of LNAI, pp. 278\u2013294. Springer, 1996.","key":"21_CR22","DOI":"10.1007\/3-540-61208-4_18"},{"doi-asserted-by":"crossref","unstructured":"R. A. Schmidt and U. Hustadt. A resolution decision procedure for fluted logic. In Proc. CADE-17, vol. 1831 of LNAI, pp. 433\u2013448. Springer, 2000.","key":"21_CR23","DOI":"10.1007\/10721959_34"},{"key":"21_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schau\u03b2","year":"1991","unstructured":"M. Schmidt-Schau\u03b2 and G. Smolka. Attributive concept descriptions with complements. J. Artificial Intelligence, 48:1\u201326, 1991.","journal-title":"J. Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T16:36:33Z","timestamp":1629563793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}