{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:14:21Z","timestamp":1743059661309,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662476710"},{"type":"electronic","value":"9783662476727"}],"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-662-47672-7_15","type":"book-chapter","created":{"date-parts":[[2015,6,19]],"date-time":"2015-06-19T10:07:39Z","timestamp":1434708459000},"page":"180-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Feasible Interpolation for QBF Resolution Calculi"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"given":"Leroy","family":"Chew","sequence":"additional","affiliation":[]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[]},{"given":"Anil","family":"Shukla","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,6,20]]},"reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02579196","volume":"7","author":"N Alon","year":"1987","unstructured":"Alon, N., Boppana, R.B.: The monotone circuit complexity of boolean functions. Combinatorica 7(1), 1\u201322 (1987)","journal-title":"Combinatorica"},{"issue":"1","key":"15_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":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"2","key":"15_CR4","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":"15_CR5","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":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"15_CR7","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In : STACS, pp. 76\u201389 (2015)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/978-3-319-15579-1_38","volume-title":"Language and Automata Theory and Applications","author":"O Beyersdorff","year":"2015","unstructured":"Beyersdorff, O., Chew, L., Sreenivasaiah, K.: A game characterisation of tree-like Q-resolution size. In: Dediu, A.-H., Formenti, E., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 486\u2013498. Springer, Heidelberg (2015)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"1\u20132","key":"15_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s00037-004-0183-5","volume":"13","author":"ML Bonet","year":"2004","unstructured":"Bonet, M.L., Domingo, C., Gavald\u00e0, R., Maciel, A., Pitassi, T.: Non-automatizability of bounded-depth Frege proofs. Computational Complexity 13(1\u20132), 47\u201368 (2004)","journal-title":"Computational Complexity"},{"issue":"6","key":"15_CR11","doi-asserted-by":"publisher","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"Maria Luisa Bonet","year":"2000","unstructured":"Maria Luisa Bonet: Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM Journal on Computing 29(6), 1939\u20131967 (2000)","journal-title":"SIAM Journal on Computing"},{"issue":"3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic 22(3), 269\u2013285 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving (2014). CoRR, abs\/1405.7253","DOI":"10.1007\/978-3-319-13770-4_11"},{"key":"15_CR14","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: IJCAI, pp. 546\u2013553 (2011)"},{"issue":"2\u20133","key":"15_CR15","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.apal.2008.09.013","volume":"157","author":"P Hrube\u0161","year":"2009","unstructured":"Hrube\u0161, P.: On lengths of proofs in non-classical logics. Annals of Pure and Applied Logic 157(2\u20133), 194\u2013205 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","volume":"577","author":"M Janota","year":"2015","unstructured":"Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"15_CR17","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"Hans Kleine B\u00fcning","year":"1995","unstructured":"Hans Kleine B\u00fcning: Marek Karpinski, and Andreas Fl\u00f6gel. Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"issue":"2","key":"15_CR18","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":"15_CR19","doi-asserted-by":"crossref","unstructured":"Kraj\u00ed\u010dek, J.: Forcing with random variables and proof complexity, vol. 382, Lecture Note Series. London Mathematical Society (2011)","DOI":"10.1017\/CBO9781139107211"},{"issue":"1","key":"15_CR20","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1006\/inco.1997.2674","volume":"140","author":"J Kraj\u00ed\u010dek","year":"1998","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P.: Some consequences of cryptographical conjectures for $$S^1_2$$ and $$EF$$. Information and Computation 140(1), 82\u201394 (1998)","journal-title":"Information and Computation"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0168-0072(84)90029-0","volume":"27","author":"D Mundici","year":"1984","unstructured":"Mundici, D.: Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity. Annals of Pure and Applied Logic 27, 265\u2013273 (1984)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"15_CR22","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. The Journal of Symbolic Logic 62(3), 981\u2013998 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"15_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":"15_CR24","unstructured":"Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: AAAI, pp. 1045\u20131050. AAAI Press (2007)"},{"key":"15_CR25","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 Van Gelder","year":"2012","unstructured":"Van Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 647\u2013663. Springer, Heidelberg (2012)"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD, pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-47672-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:12:51Z","timestamp":1676945571000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-47672-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662476710","9783662476727"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-47672-7_15","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":"20 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}