{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T05:02:50Z","timestamp":1780981370435,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642390708","type":"print"},{"value":"9783642390715","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_7","type":"book-chapter","created":{"date-parts":[[2013,6,23]],"date-time":"2013-06-23T21:23:17Z","timestamp":1372022597000},"page":"67-82","source":"Crossref","is-referenced-by-count":14,"title":["On Propositional QBF Expansions and Q-Resolution"],"prefix":"10.1007","author":[{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.: QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 187\u2013201. Springer, Heidelberg (2002)"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V. Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods in System Design\u00a041(1), 45\u201365 (2012)","journal-title":"Formal Methods in System Design"},{"key":"7_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-32275-7_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Evaluating QBFs via symbolic Skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 285\u2013300. Springer, Heidelberg (2005)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"7_CR5","unstructured":"Bubeck, U.: Model-based transformations for quantified Boolean formulas. Ph.D. thesis, University of Paderborn (2010)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-72788-0_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"U. Bubeck","year":"2007","unstructured":"Bubeck, U., B\u00fcning, H.K.: Bounded universal expansion for preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 244\u2013257. Springer, Heidelberg (2007)"},{"key":"7_CR7","unstructured":"B\u00fcning, H.K., Bubeck, U.: Theory of quantified boolean formulas. In: Handbook of Satisfiability. IOS Press (2009)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1) (1995)","DOI":"10.1006\/inco.1995.1025"},{"issue":"2","key":"7_CR9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M. Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. J. Autom. Reasoning\u00a028(2), 101\u2013142 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","year":"2012","unstructured":"Cimatti, A., Sebastiani, R. (eds.): SAT 2012. LNCS, vol.\u00a07317. Springer, Heidelberg (2012)"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S.A. Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log.\u00a044(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Egly, U.: On sequent systems and resolution for QBFs. In: Cimatti, Sebastiani (eds.) [10], pp. 100\u2013113","DOI":"10.1007\/978-3-642-31612-8_9"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: QuBE 7.0 system description. Journal on Satisfiability, Boolean Modeling and Computation 7 (2010)","DOI":"10.3233\/SAT190079"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E. Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/term resolution and learning in the evaluation of quantified Boolean formulas. Journal of Artificial Intelligence Research\u00a026(1), 371\u2013416 (2006)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. In: Cimatti, Sebastiani (eds.) [10], pp. 114\u2013128","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W. Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"issue":"1","key":"7_CR18","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1002\/malq.19900360106","volume":"36","author":"J. Kraj\u00ed\u010dek","year":"1990","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P.: Quantified propositional calculi and fragments of bounded arithmetic. Mathematical Logic Quarterly\u00a036(1), 29\u201346 (1990)","journal-title":"Mathematical Logic Quarterly"},{"key":"7_CR19","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":"7_CR20","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT (2010)","DOI":"10.3233\/SAT190077"},{"key":"7_CR21","unstructured":"Rintanen, J.: Improvements to the evaluation of quantified Boolean formulae. In: Dean, T. (ed.) IJCAI, pp. 1192\u20131197. Morgan Kaufmann (1999)"},{"key":"7_CR22","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bulletin of the EATCS 64 (1998)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T04:52:26Z","timestamp":1780980746000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}