{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:27:43Z","timestamp":1725863263870},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319449524"},{"type":"electronic","value":"9783319449531"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-44953-1_7","type":"book-chapter","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T11:12:23Z","timestamp":1471864343000},"page":"96-112","source":"Crossref","is-referenced-by-count":10,"title":["Dependency Schemes in QBF Calculi: Semantics and Soundness"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Blinkhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,23]]},"reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Jiang, J.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter)models from long-distance resolution proofs. In: Conference on Artificial Intelligence (AAAI), pp. 3694\u20133701 (2015)","DOI":"10.1609\/aaai.v29i1.9750"},{"key":"7_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)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Proceedings of the ACM Conference on Innovations in Theoretical Computer Science (ITCS 2016), pp. 249\u2013260. ACM (2016)","DOI":"10.1145\/2840728.2840740"},{"key":"7_CR5","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":"7_CR6","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: International Symposium on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 30, pp. 76\u201389 (2015)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/978-3-662-47672-7_15","volume-title":"Automata, Languages, and Programming","author":"O Beyersdorff","year":"2015","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9134, pp. 180\u2013192. Springer, Heidelberg (2015)"},{"key":"7_CR8","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not simple. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS 2016) (2016)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/978-3-642-14186-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158\u2013171. Springer, Heidelberg (2010)"},{"key":"7_CR10","unstructured":"Bubeck, U.: Model-based Transformations for Quantified Boolean Formulas. Ph.D. thesis (2010)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"7_CR13","doi-asserted-by":"crossref","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. Theorical Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theorical Comput. Sci."},{"issue":"1","key":"7_CR14","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"7_CR15","unstructured":"Lonsing, F.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.D. thesis, Johannes Kepler University (2012)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-24318-4_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Lonsing","year":"2015","unstructured":"Lonsing, F., Egly, U.: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API. In: Heule, M., et al. (eds.) SAT 2015. LNCS, vol. 9340, pp. 191\u2013198. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_14"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/978-3-540-89439-1_36","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Samer","year":"2008","unstructured":"Samer, M.: Variable dependencies of quantified CSPs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 512\u2013527. Springer, Heidelberg (2008)"},{"issue":"1","key":"7_CR18","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified boolean formulas. J. Autom. Reasoning 42(1), 77\u201397 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: International Conference on Principles and Practice of Constraint Programming (CP), pp. 578\u2013592 (2005)","DOI":"10.1007\/11564751_43"},{"key":"7_CR20","unstructured":"Slivovsky, F.: Structure in #SAT and QBF. Ph.D. thesis, Vienna University of Technology (2015)"},{"key":"7_CR21","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/j.tcs.2015.10.020","volume":"612","author":"F Slivovsky","year":"2016","unstructured":"Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. TCS 612, 83\u2013101 (2016)","journal-title":"TCS"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Annual Symposium on Theory of Computing, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"789","DOI":"10.1007\/978-3-642-23786-7_59","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"A Gelder Van","year":"2011","unstructured":"Van Gelder, A.: Variable independence and resolution paths for quantified boolean formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789\u2013803. Springer, Heidelberg (2011)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A Gelder Van","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":"7_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: International Conference on Computer-aided Design (ICCAD), pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44953-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,6]],"date-time":"2022-07-06T17:21:13Z","timestamp":1657128073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44953-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319449524","9783319449531"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44953-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}