{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:17Z","timestamp":1759638917740,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_20","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"314-325","source":"Crossref","is-referenced-by-count":5,"title":["A Resolution-Style Proof System for DQBF"],"prefix":"10.1007","author":[{"given":"Markus N.","family":"Rabe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","volume":"523","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Chiang, H.J.K., Jiang, J.H.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86\u2013100 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-319-40970-2_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"O Beyersdorff","year":"2016","unstructured":"Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculi to DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 490\u2013499. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_30"},{"key":"20_CR3","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. 3542, pp. 59\u201370. Springer, Heidelberg (2005). doi: 10.1007\/11527695_5"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_10"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/11916277_38","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Bruttomesso","year":"2006","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Santuari, A., Sebastiani, R.: To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in $$\\mathit{SMT}(\\cal{EUF} \\cup \\cal{T})$$ . In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 557\u2013571. Springer, Heidelberg (2006). doi: 10.1007\/11916277_38"},{"issue":"1","key":"20_CR6","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK Buning","year":"1995","unstructured":"Buning, H.K., Karpinski, M., Flogel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"issue":"3","key":"20_CR7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201\u2013215 (1960)","journal-title":"J. ACM (JACM)"},{"key":"20_CR8","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: 3 encodings of reactive synthesis. In: Proceedings of QUANTIFY, pp. 20\u201322 (2015)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54577-5_20"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proceedings of LICS, Washington, DC, USA, pp. 321\u2013330. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.53"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-09284-3_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243\u2013251. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_19"},{"key":"20_CR12","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Proceedings of Pragmatics of SAT 2012 (2012)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Proceedings of Pragmatics of SAT, pp. 103\u2013116 (2014)","DOI":"10.29007\/1s5k"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified Boolean formulae. In: Proceedings of ICCD, pp. 396\u2013403, October 2013","DOI":"10.1109\/ICCD.2013.6657071"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Proceedings of DATE (2015)","DOI":"10.7873\/DATE.2015.0098"},{"key":"20_CR16","unstructured":"Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean formulas satisfiability library (QBFLIB) (2005). www.qbflib.org"},{"key":"20_CR17","first-page":"167","volume":"30","author":"L Henkin","year":"1961","unstructured":"Henkin, L.: Some remarks on infinitely long formulas. J. Symb. Logic 30, 167\u2013183 (1961)","journal-title":"J. Symb. Logic"},{"key":"20_CR18","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings of IJCAI, pp. 325\u2013331. AAAI Press (2015)"},{"key":"20_CR19","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. 6695, pp. 230\u2013244. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21581-0_19"},{"issue":"2\u20133","key":"20_CR20","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. JSAT 7(2\u20133), 71\u201376 (2010)","journal-title":"JSAT"},{"issue":"7","key":"20_CR21","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"G Peterson","year":"2001","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Comput. Math. Appl. 41(7), 957\u2013992 (2001)","journal-title":"Comput. Math. Appl."},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: Proceedings of FOCS, pp. 348\u2013363. IEEE (1979)","DOI":"10.1109\/SFCS.1979.25"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-40970-2_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MN Rabe","year":"2016","unstructured":"Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375\u2013392. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_23"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Leander Tentrup, C.: A certifying QBF solver. In: Proceedings of FMCAD, pp. 136\u2013143 (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"20_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1","volume-title":"Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970","author":"J Siekmann","year":"1983","unstructured":"Siekmann, J., Wrightson, G.: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970. Springer, Heidelberg (1983). doi: 10.1007\/978-3-642-81955-1"},{"key":"20_CR26","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of CAD, pp. 220\u2013227. IEEE (1997)"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_24"},{"key":"20_CR28","series-title":"LNCS","first-page":"475","volume-title":"CAV 2017","author":"L Tentrup","year":"2017","unstructured":"Tentrup, L.: On expansion and resolution in CEGAR based QBF solving. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 475\u2013494. Springer, Cham (2017)"},{"key":"20_CR29","first-page":"115","volume":"2","author":"GS Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Constr. Math. Math. Logic 2, 115\u2013125 (1968). Reprinted in [2]: 10\u201313","journal-title":"Stud. Constr. Math. Math. Logic"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A Gelder","year":"2012","unstructured":"Gelder, A.: Contributions to the theory of practical quantified Boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, pp. 647\u2013663. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33558-7_47"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-24318-4_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"R Wimmer","year":"2015","unstructured":"Wimmer, R., Gitina, K., Nist, J., Scholl, C., Becker, B.: Preprocessing for DQBF. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 173\u2013190. Springer, Cham (2015). doi: 10.1007\/978-3-319-24318-4_13"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre-an effective preprocessor for QBF and DQBF. In: Proceedings of TACAS (2017)","DOI":"10.1007\/978-3-662-54577-5_21"},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of ICCAD, pp. 442\u2013449, November 2002","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:59:54Z","timestamp":1750798794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}