{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:13Z","timestamp":1725533893711},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_36","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"391-397","source":"Crossref","is-referenced-by-count":3,"title":["Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits"],"prefix":"10.1007","author":[{"given":"Hans","family":"Kleine B\u00fcning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xishun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Bubeck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"36_CR1","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00289267","volume":"15","author":"S. Anderaa","year":"1981","unstructured":"Anderaa, S., B\u00f6rger, E.: The Equivalence of Horn and Network Complexity for Boolean Functions. Acta Informatica\u00a015, 303\u2013307 (1981)","journal-title":"Acta Informatica"},{"issue":"2","key":"36_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1811123.1811124","volume":"5","author":"M. Bauer","year":"1973","unstructured":"Bauer, M., Brand, D., Fischer, M., Meyer, A., Paterson, M.: A Note on Disjunctive Form Tautologies. SIGACT News\u00a05(2), 17\u201320 (1973)","journal-title":"SIGACT News"},{"issue":"10","key":"36_CR3","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1016\/j.dam.2007.10.005","volume":"156","author":"U. Bubeck","year":"2008","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Models and Quantifier Elimination for Quantified Horn Formulas. Discrete Applied Mathematics\u00a0156(10), 1606\u20131622 (2008)","journal-title":"Discrete Applied Mathematics"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-54487-9_57","volume-title":"Computer Science Logic","author":"A. Fl\u00f6gel","year":"1991","unstructured":"Fl\u00f6gel, A., Karpinski, M., Kleine B\u00fcning, H.: Subclasses of Quantified Boolean Formulas. In: Sch\u00f6nfeld, W., B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1990. LNCS, vol.\u00a0533, pp. 145\u2013155. Springer, Heidelberg (1991)"},{"issue":"1","key":"36_CR5","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(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-50241-6_34","volume-title":"CSL \u201987","author":"M. Karpinski","year":"1988","unstructured":"Karpinski, M., Kleine B\u00fcning, H., Schmitt, P.: On the computational complexity of quantified Horn clauses. In: CSL 1987. LNCS, vol.\u00a0329, pp. 129\u2013137. Springer, Heidelberg (1988)"},{"key":"36_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-79719-7_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"F. Lonsing","year":"2008","unstructured":"Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF Solving. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 196\u2013210. Springer, Heidelberg (2008)"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/11814948_35","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A. Sabharwal","year":"2006","unstructured":"Sabharwal, A., Ansotegui, C., Gomes, C., Hart, J., Selman, B.: QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 382\u2013395. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T20:11:00Z","timestamp":1552075860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}