{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T17:27:54Z","timestamp":1742923674418,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319155784"},{"type":"electronic","value":"9783319155791"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15579-1_38","type":"book-chapter","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T08:36:13Z","timestamp":1424680573000},"page":"486-498","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Game Characterisation of Tree-like Q-resolution Size"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"given":"Leroy","family":"Chew","sequence":"additional","affiliation":[]},{"given":"Karteek","family":"Sreenivasaiah","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,2,24]]},"reference":[{"issue":"3","key":"38_CR1","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.jcss.2007.06.025","volume":"74","author":"A Atserias","year":"2008","unstructured":"Atserias, A., Dalmau, V.: A combinatorial characterization of resolution width. Journal of Computer and System Sciences 74(3), 323\u2013334 (2008)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"38_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 41(1), 45\u201365 (2012)","journal-title":"Formal Methods in System Design"},{"key":"38_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-319-09284-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154\u2013169. Springer, Heidelberg (2014)"},{"key":"38_CR4","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Harsha, P.,: Lower bounds for bounded depth Frege proofs via Buss-Pudl\u00e1k games. ACM Trans. on Computational Logic 11(3) (2010)","DOI":"10.1145\/1740582.1740587"},{"issue":"2","key":"38_CR5","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. Journal of the ACM 48(2), 149\u2013169 (2001)","journal-title":"Journal of the ACM"},{"issue":"1\u20134","key":"38_CR6","first-page":"133","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: Experience and perspectives. JSAT 5(1\u20134), 133\u2013191 (2008)","journal-title":"JSAT"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-662-44465-8_8","volume-title":"Mathematical Foundations of Computer Science 2014","author":"O Beyersdorff","year":"2014","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014, Part II. LNCS, vol. 8635, pp. 81\u201393. Springer, Heidelberg (2014)"},{"key":"38_CR8","first-page":"120","volume":"21","author":"O Beyersdorff","year":"2014","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. ECCC 21, 120 (2014)","journal-title":"ECCC"},{"issue":"23","key":"38_CR9","doi-asserted-by":"publisher","first-page":"1074","DOI":"10.1016\/j.ipl.2010.09.007","volume":"110","author":"O Beyersdorff","year":"2010","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Information Processing Letters 110(23), 1074\u20131077 (2010)","journal-title":"Information Processing Letters"},{"issue":"18","key":"38_CR10","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2013.06.002","volume":"113","author":"O Beyersdorff","year":"2013","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A characterization of tree-like resolution size. Information Processing Letters 113(18), 666\u2013671 (2013)","journal-title":"Information Processing Letters"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.,: Parameterized complexity of DPLL search procedures. ACM Trans. on Computational Logic 14(3) (2013)","DOI":"10.1145\/2499937.2499941"},{"key":"38_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-09284-3_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"O Beyersdorff","year":"2014","unstructured":"Beyersdorff, O., Kullmann, O.: Unified characterisations of resolution hardness measures. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 170\u2013187. Springer, Heidelberg (2014)"},{"issue":"7","key":"38_CR13","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1016\/j.apal.2011.09.009","volume":"163","author":"SR Buss","year":"2012","unstructured":"Buss, S.R.: Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic 163(7), 906\u2013917 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"38_CR14","doi-asserted-by":"crossref","unstructured":"Cook, S.A., Nguyen, P.: Logical Foundations of Proof Complexity. Cambridge University Press (2010)","DOI":"10.1017\/CBO9780511676277"},{"key":"38_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-31612-8_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"U Egly","year":"2012","unstructured":"Egly, U.: On sequent systems and resolution for QBFs. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 100\u2013113. Springer, Heidelberg (2012)"},{"key":"38_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-45221-5_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"U Egly","year":"2013","unstructured":"Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 291\u2013308. Springer, Heidelberg (2013)"},{"issue":"6","key":"38_CR17","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1016\/S0020-0190(03)00345-4","volume":"87","author":"JL Esteban","year":"2003","unstructured":"Esteban, J.L., Tor\u00e1n, J.: A combinatorial characterization of treelike resolution space. Information Processing Letters 87(6), 295\u2013300 (2003)","journal-title":"Information Processing Letters"},{"key":"38_CR18","unstructured":"Janota, M., Marques-Silva, J.: $$\\forall $$Exp+Res does not p-simulate Q-resolution. International Workshop on Quantified Boolean Formulas (2013)"},{"key":"38_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-39071-5_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"M Janota","year":"2013","unstructured":"Janota, M., Marques-Silva, J.: On propositional QBF expansions and Q-resolution. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 67\u201382. Springer, Heidelberg (2013)"},{"issue":"1","key":"38_CR20","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"38_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory","author":"J Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press, Cambridge (1995)"},{"issue":"2","key":"38_CR22","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"38_CR23","doi-asserted-by":"crossref","unstructured":"Pudl\u00e1k, P.: Proofs as games. American Math. Monthly, pp. 541\u2013550 (2000)","DOI":"10.1080\/00029890.2000.12005233"},{"key":"38_CR24","unstructured":"Pudl\u00e1k, P., Impagliazzo, R.: A lower bound for DLL algorithms for SAT. In: Proc. 11th Symposium on Discrete Algorithms, pp. 128\u2013136 (2000)"},{"key":"38_CR25","unstructured":"Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: AAAI, pp. 1045\u20131050. AAAI Press, (2007)"},{"issue":"4","key":"38_CR26","doi-asserted-by":"publisher","first-page":"417","DOI":"10.2178\/bsl\/1203350879","volume":"13","author":"N Segerlind","year":"2007","unstructured":"Segerlind, N.: The complexity of propositional proofs. Bulletin of Symbolic Logic 13(4), 417\u2013481 (2007)","journal-title":"Bulletin of Symbolic Logic"},{"key":"38_CR27","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Contributions to the theory of practical quantified Boolean formula solving. In: CP, pp. 647\u2013663 (2012)","DOI":"10.1007\/978-3-642-33558-7_47"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15579-1_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T07:49:36Z","timestamp":1675842576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15579-1_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319155784","9783319155791"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15579-1_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"24 February 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}