{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T04:09:37Z","timestamp":1750392577216,"version":"3.41.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319614663"},{"type":"electronic","value":"9783319614670"}],"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-61467-0_8","type":"book-chapter","created":{"date-parts":[[2017,6,17]],"date-time":"2017-06-17T04:33:58Z","timestamp":1497674038000},"page":"129-138","source":"Crossref","is-referenced-by-count":2,"title":["Skolem Function Continuation for Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Katalin","family":"Fazekas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,18]]},"reference":[{"key":"8_CR1","unstructured":"Kleine B\u00fcning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Handbook of Satisfiability, pp. 735\u2013760. IOS Press (2009)"},{"issue":"1\u20134","key":"8_CR2","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":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1\u201320. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54013-4_1"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-319-13770-4_11","volume-title":"Artificial Intelligence and Symbolic Computation","author":"U Egly","year":"2014","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. In: Aranda-Corral, G.A., Calmet, J., Mart\u00edn-Mateos, F.J. (eds.) AISC 2014. LNCS, vol. 8884, pp. 120\u2013131. Springer, Cham (2014). doi: 10.1007\/978-3-319-13770-4_11"},{"key":"8_CR5","unstructured":"Balabanov, V., Jiang, J.R., Scholl, C.: Skolem functions computation for CEGAR based QBF solvers. In: QBF (2015)"},{"key":"8_CR6","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"},{"issue":"1","key":"8_CR7","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. Form. Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR8","unstructured":"Benedetti, M.: Extracting certificates from quantified Boolean formulas. In: IJCAI, pp. 47\u201353. Professional Book Center (2005)"},{"issue":"4","key":"8_CR9","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/AIC-2009-0468","volume":"22","author":"M Narizzano","year":"2009","unstructured":"Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFs: a comparison of state-of-the-art tools. AI Commun. 22(4), 191\u2013210 (2009)","journal-title":"AI Commun."},{"key":"8_CR10","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":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A., Sinz, C., Kr\u00f6ning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201\u2013214. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72788-0_21"},{"issue":"1","key":"8_CR12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10817-016-9390-4","volume":"58","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97\u2013125 (2017)","journal-title":"J. Autom. Reason."},{"key":"8_CR13","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\/AAAI, pp. 546\u2013553 (2011)"},{"key":"8_CR14","unstructured":"Van Gelder, A.: Certificate extraction from variable-elimination QBF preprocessors. In: QBF, pp. 35\u201339 (2013)"},{"issue":"1","key":"8_CR15","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":"8_CR16","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified Boolean formulas. In: Handbook of Satisfiability, pp. 761\u2013780. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-761"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: FMCAD, pp. 136\u2013143 (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"8_CR18","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."},{"issue":"1\u20132","key":"8_CR19","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":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-642-45221-5_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Janota","year":"2013","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: On QBF proofs and preprocessing. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 473\u2013489. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_32"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","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, vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_10"},{"key":"8_CR22","unstructured":"Lonsing, F., Egly, U.: DepQBF: an incremental QBF solver based on clause groups. CoRR abs\/1502.02484 (2015)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-61467-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T18:39:23Z","timestamp":1750358363000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-61467-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319614663","9783319614670"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-61467-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}