{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T04:59:31Z","timestamp":1777870771652,"version":"3.51.4"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319630458","type":"print"},{"value":"9783319630465","type":"electronic"}],"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-63046-5_23","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"371-384","source":"Crossref","is-referenced-by-count":45,"title":["DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL"],"prefix":"10.1007","author":[{"given":"Florian","family":"Lonsing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Egly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"23_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. 2517, pp. 187\u2013201. Springer, Heidelberg (2002). doi: 10.1007\/3-540-36126-X_12"},{"issue":"1","key":"23_CR2","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":"23_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, Cham (2014). doi: 10.1007\/978-3-319-09284-3_12"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-44953-1_7","volume-title":"Principles and Practice of Constraint Programming","author":"O Beyersdorff","year":"2016","unstructured":"Beyersdorff, O., Blinkhorn, J.: Dependency schemes in QBF calculi: semantics and soundness. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 96\u2013112. Springer, Cham (2016). doi: 10.1007\/978-3-319-44953-1_7"},{"key":"23_CR5","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: STACS. LIPIcs, vol. 30, pp. 76\u201389. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)"},{"key":"23_CR6","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":"23_CR7","unstructured":"Bogaerts, B., Janhunen, T., Tasharrofi, S.: SAT-to-SAT in QBFEval 2016. In: QBF Workshop. CEUR Workshop Proceedings, vol. 1719, pp. 63\u201370. CEUR-WS.org (2016)"},{"key":"23_CR8","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., Kleine B\u00fcning, H.: Bounded universal expansion for preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244\u2013257. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72788-0_24"},{"key":"23_CR9","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: AAAI, pp. 262\u2013267. AAAI Press\/The MIT Press (1998)"},{"issue":"5","key":"23_CR10","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"7","key":"23_CR11","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"1","key":"23_CR12","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10472-016-9501-2","volume":"80","author":"U Egly","year":"2017","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80(1), 21\u201345 (2017)","journal-title":"Ann. Math. Artif. Intell."},{"key":"23_CR13","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 2013. LNCS, vol. 8312, pp. 291\u2013308. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_21"},{"key":"23_CR14","doi-asserted-by":"crossref","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. JAIR 26, 371\u2013416 (2006)","journal-title":"JAIR"},{"key":"23_CR15","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. JAIR 53, 127\u2013168 (2015)","journal-title":"JAIR"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-40970-2_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Janota","year":"2016","unstructured":"Janota, M.: On Q-resolution and CDCL QBF solving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 402\u2013418. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_25"},{"key":"23_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","volume":"234","author":"M Janota","year":"2016","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"Artif. Intell."},{"key":"23_CR18","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. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR19","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: IJCAI, pp. 325\u2013331. AAAI Press (2015)"},{"key":"23_CR20","unstructured":"Kleine B\u00fcning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Handbook of Satisfiability, FAIA, vol. 185, pp. 735\u2013760. IOS Press (2009)"},{"issue":"1","key":"23_CR21","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":"23_CR22","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. 6175, pp. 128\u2013142. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_12"},{"key":"23_CR23","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Ferm\u00fcller, C.G. (eds.) TABLEAUX 2002. LNCS, vol. 2381, pp. 160\u2013175. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45616-3_12"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-662-48899-7_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Lonsing","year":"2015","unstructured":"Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 418\u2013433. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_29"},{"issue":"2\u20133","key":"23_CR26","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"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-642-14186-7_14"},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-10428-7_38","volume-title":"Principles and Practice of Constraint Programming","author":"F Lonsing","year":"2014","unstructured":"Lonsing, F., Egly, U.: Incremental QBF solving. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 514\u2013530. Springer, Cham (2014). doi: 10.1007\/978-3-319-10428-7_38"},{"key":"23_CR29","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., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 191\u2013198. Springer, Cham (2015). doi: 10.1007\/978-3-319-24318-4_14"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. CoRR abs\/1702.08256 (2017). http:\/\/arxiv.org\/abs\/1702.08256 , CADE 2017 proceedings version with appendix","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"23_CR31","unstructured":"Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. CoRR abs\/1701.06612 (2017). http:\/\/arxiv.org\/abs\/1701.06612 , technical report"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-40970-2_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"F Lonsing","year":"2016","unstructured":"Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 435\u2013452. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_27"},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39071-5_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"F Lonsing","year":"2013","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient clause learning for quantified boolean formulas via QBF pseudo unit propagation. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 100\u2013115. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39071-5_9"},{"key":"23_CR34","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1016\/j.artint.2016.04.002","volume":"237","author":"F Lonsing","year":"2016","unstructured":"Lonsing, F., Seidl, M., Van Gelder, A.: The QBF gallery: behind the scenes. Artif. Intell. 237, 92\u2013114 (2016)","journal-title":"Artif. Intell."},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Verification of partial designs using incremental QBF solving. In: DATE, pp. 623\u2013628. IEEE (2012)","DOI":"10.1109\/DATE.2012.6176547"},{"issue":"1\u20132","key":"23_CR36","doi-asserted-by":"crossref","first-page":"133","DOI":"10.3233\/FI-2016-1445","volume":"149","author":"P Marin","year":"2016","unstructured":"Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows. Fundam. Inform. 149(1\u20132), 133\u2013158 (2016)","journal-title":"Fundam. Inform."},{"key":"23_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430\u2013435. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_33"},{"key":"23_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-319-40970-2_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"T Peitl","year":"2016","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Long distance Q-resolution with dependency schemes. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 500\u2013518. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_31"},{"key":"23_CR39","unstructured":"Pulina, L.: The ninth QBF solvers evaluation - preliminary report. In: Proceedings of the 4th International Workshop on Quantified Boolean Formulas QBF 2016. CEUR Workshop Proceedings, vol. 1719, pp. 1\u201313. CEUR-WS.org (2016)"},{"key":"23_CR40","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: FMCAD, pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"issue":"1","key":"23_CR41","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"1","key":"23_CR42","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. JAR 42(1), 77\u201397 (2009)","journal-title":"JAR"},{"key":"23_CR43","unstructured":"Scholl, C., Pigorsch, F.: The QBF solver AIGSolve. In: QBF Workshop. CEUR Workshop Proceedings, vol. 1719, pp. 55\u201362. CEUR-WS.org (2016)"},{"key":"23_CR44","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, FAIA, vol. 185, pp. 131\u2013153. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"23_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-31612-8_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"F Slivovsky","year":"2012","unstructured":"Slivovsky, F., Szeider, S.: Computing resolution-path dependencies in linear time. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 58\u201371. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_6"},{"key":"23_CR46","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. Theor. Comput. Sci. 612, 83\u2013101 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 Van Gelder","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). doi: 10.1007\/978-3-642-23786-7_59"},{"key":"23_CR48","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, pp. 647\u2013663. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33558-7_47"},{"key":"23_CR49","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442\u2013449. ACM\/IEEE Computer Society (2002)","DOI":"10.1145\/774572.774637"},{"key":"23_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200\u2013215. Springer, Heidelberg (2002). doi: 10.1007\/3-540-46135-3_14"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:56Z","timestamp":1750533896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}