{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:03:33Z","timestamp":1777125813651,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540727873","type":"print"},{"value":"9783540727880","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72788-0_21","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T08:25:22Z","timestamp":1183019122000},"page":"201-214","source":"Crossref","is-referenced-by-count":30,"title":["A First Step Towards a Unified Proof Checker for QBF"],"prefix":"10.1007","author":[{"given":"Toni","family":"Jussila","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kr\u00f6ning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L.J. Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The polynomial\u2013time hierarchy. TCS\u00a03, 1\u201322 (1976)","journal-title":"TCS"},{"key":"21_CR2","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, New York (1979)"},{"key":"21_CR3","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research\u00a010, 323\u2013352 (1999)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"21_CR4","unstructured":"Otwell, C., Remshagen, A., Truemper, K.: An effective QBF solver for planning problems. In: MSV\/AMCS, pp. 311\u2013316. CSREA Press (2004)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/11527695_9","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Giunchiglia","year":"2005","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QBF reasoning on real\u2013world instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 105\u2013121. Springer, Heidelberg (2005)"},{"issue":"3","key":"21_CR6","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R.E. Ladner","year":"1977","unstructured":"Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing\u00a06(3), 467\u2013480 (1977), http:\/\/link.aip.org\/link\/?SMJ\/6\/467\/1 , doi:10.1137\/0206033","journal-title":"SIAM Journal on Computing"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., et al.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_4","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"21_CR9","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. In: Proc.\u00a04th Intl.\u00a0Work.\u00a0on Bounded Model Checking (BMC). To be published in ENTCS, Elsevier, Amsterdam (2006)"},{"key":"21_CR10","unstructured":"Benedetti, M.: Experimenting with QBF-based formal verification. In: Proc. of the 3rd International Workshop on Constraints in Formal Verification (CFV). To be published in ENTCS, Elsevier, Amsterdam (2005)"},{"issue":"2","key":"21_CR11","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0166-218X(02)00409-2","volume":"130","author":"D.A. Plaisted","year":"2003","unstructured":"Plaisted, D.A., Biere, A., Zhu, Y.: A satisfiability procedure for quantified boolean formulae. Discrete Appl. Math.\u00a0130(2), 291\u2013328 (2003)","journal-title":"Discrete Appl. Math."},{"key":"21_CR12","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: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"},{"key":"21_CR13","series-title":"Lecture Notes in Artificial Intelligence","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. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"21_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QUBE: A system for deciding quantified boolean formulas satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"},{"key":"21_CR15","first-page":"262","volume-title":"Proc. of AAAI\/IAAI","author":"M. Cadoli","year":"1998","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Proc. of AAAI\/IAAI, pp. 262\u2013267. AAAI Press, Menlo Park (1998)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/11564751_43","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"H. Samulowitz","year":"2005","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 578\u2013592. Springer, Heidelberg (2005)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/978-3-540-30201-8_34","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G. Pan","year":"2004","unstructured":"Pan, G., Vardi, M.Y.: Symbolic decision procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 453\u2013467. Springer, Heidelberg (2004)"},{"key":"21_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/978-3-540-32275-7_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Evaluating QBFs via symbolic skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 285\u2013300. Springer, Heidelberg (2005)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_33","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Bacchus, F.: Binary clause reasoning in QBF. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, Springer, Heidelberg (2006)"},{"key":"21_CR21","first-page":"145","volume":"2","author":"M. Narizzano","year":"2006","unstructured":"Narizzano, M., Tacchella, A., Pulina, L.: Report of the third QBF solvers evaluation. JSAT\u00a02, 145\u2013164 (2006)","journal-title":"JSAT"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, vol. 2, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"21_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"21_CR24","doi-asserted-by":"publisher","first-page":"1047","DOI":"10.1145\/1120725.1120821","volume-title":"Proc. of ASP-DAC","author":"Y. Yu","year":"2005","unstructured":"Yu, Y., Malik, S.: Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In: Proc. of ASP-DAC, pp. 1047\u20131051. ACM Press, New York (2005)"},{"issue":"1","key":"21_CR25","doi-asserted-by":"publisher","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\u00fcgel, A.: Resolution for quantified boolean formulas. Inf. Comput.\u00a0117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-540-25967-1_3","volume-title":"Logic versus Approximation","author":"H. Kleine B\u00fcning","year":"2004","unstructured":"Kleine B\u00fcning, H., Zhao, X.: On models for quantified boolean formulas. In: Lenski, W. (ed.) Logic versus Approximation. LNCS, vol.\u00a03075, pp. 18\u201332. Springer, Heidelberg (2004)"},{"key":"21_CR27","unstructured":"Benedetti, M.: Extracting certificates from quantified boolean formulas. In: Proc. of IJCAI, pp. 47\u201353 (2005)"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-24605-3_8","volume-title":"Theory and Applications of Satisfiability Testing","author":"H.K. B\u00fcning","year":"2004","unstructured":"B\u00fcning, H.K., Subramani, K., Zhao, X.: On boolean models for quantified boolean horn formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 93\u2013104. Springer, Heidelberg (2004)"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C. Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol.\u00a03967, pp. 600\u2013611. Springer, Heidelberg (2006)"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11814948_8","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"T. Jussila","year":"2006","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 54\u201360. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72788-0_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:05:07Z","timestamp":1605744307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72788-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727873","9783540727880"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72788-0_21","relation":{},"subject":[]}}