{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T10:08:54Z","timestamp":1790244534001,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540208518","type":"print"},{"value":"9783540246053","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_8","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:50:35Z","timestamp":1280379035000},"page":"93-104","source":"Crossref","is-referenced-by-count":12,"title":["On Boolean Models for Quantified Boolean Horn Formulas"],"prefix":"10.1007","author":[{"given":"Hans","family":"Kleine B\u00fcning","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xishun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.E.: A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Information Processing Letters\u00a08, 121\u2013123 (1979)","journal-title":"Information Processing Letters"},{"key":"8_CR2","volume-title":"Highlights of Satisfiability Research in the Year 2000","author":"M. Cadoli","year":"2000","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulas and its Evaluation. In: Highlights of Satisfiability Research in the Year 2000. IOS Press, Amsterdam (2000)"},{"key":"8_CR3","first-page":"119","volume":"28","author":"S. Cook","year":"1999","unstructured":"Cook, S., Soltys, M.: Boolean Programs and Quantified Propositional Proof Systems. Bulletin of the Section of Logic\u00a028, 119\u2013129 (1999)","journal-title":"Bulletin of the Section of Logic"},{"key":"8_CR4","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, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"8_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0515-9","volume-title":"Parameterized Complexity","author":"R. Downey","year":"1999","unstructured":"Downey, R., Fellows, M.: Parameterized Complexity. Springer, New York (1999)"},{"key":"8_CR6","unstructured":"Feldmann, R., Monien, B., Schambergers, S.: A Distributed Algorithm to Evaluate Quantified Boolean Formulas. In: proceedings of AAAI (2000)"},{"key":"8_CR7","unstructured":"Fl\u00f6gel, A.: Resolution f\u00fcr quantifizierte Bool\u2019sche Formeln, Ph. D thesis, Universit\u00e4t Paderborn (1993)"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"A. Fl\u00f6gel","year":"1995","unstructured":"Fl\u00f6gel, A., Karpinski, M., Kleine B\u00fcning, H.: Resolution for Quantified Boolean Formulas. Information and Computation\u00a0117, 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"8_CR9","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman Company, San Francisco (1979)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: A System for Deciding Quantified Boolean Formulas. In: Proceedings of IJCAR, Siena (2001)","DOI":"10.1007\/3-540-45744-5_27"},{"key":"8_CR11","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. Theoretical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"8_CR12","volume-title":"Propositional Logic: Deduction and Algorithms","author":"H. Kleine B\u00fcning","year":"1999","unstructured":"Kleine B\u00fcning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: Lean Clause-Sets: Generalizations of Minimal Unsatisfiable Clause- Sets. To appear in Discrete Applied Mathematics (2003)","DOI":"10.1016\/S0166-218X(02)00406-7"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Letz, R.: Advances in Decision Procedure for Quantified Boolean Formulas. In: Proceedings of IJCAR, Siena (2001)","DOI":"10.1007\/3-540-45616-3_12"},{"key":"8_CR15","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"8_CR16","unstructured":"Rintanen, J.T.: Improvements to the Evaluation of Quantified Boolean Formulae. In: Proceedings of IJCAI (1999)"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1145\/800133.804350","volume-title":"Proceedings of the 10th Annual ACM Symposium on Theory of Computing","author":"T.J. Schaefer","year":"1978","unstructured":"Schaefer, T.J.: The Complexity of Satisfiability Problem. In: Aho, A. (ed.) Proceedings of the 10th Annual ACM Symposium on Theory of Computing, pp. 216\u2013226. ACM Press, New York City (1978)"},{"key":"8_CR18","unstructured":"Szeider, S.: Generalization of Matched CNF Formulas. In: 5th International Symposium on Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, USA (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:53:53Z","timestamp":1559332433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}