{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:55Z","timestamp":1725559255459},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_32","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"466-480","source":"Crossref","is-referenced-by-count":2,"title":["Validating QBF Invalidity in HOL4"],"prefix":"10.1007","author":[{"given":"Tjark","family":"Weber","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","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., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-540-27813-9_31","volume-title":"Computer Aided Verification","author":"G. Gopalakrishnan","year":"2004","unstructured":"Gopalakrishnan, G., Yang, Y., Sivaraj, H.: QB or not QB: An efficient execution verification tool for memory orderings. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 401\u2013413. Springer, Heidelberg (2004)"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","first-page":"408","volume-title":"Theory and Applications of Satisfiability Testing","author":"Z. Hanna","year":"2005","unstructured":"Hanna, Z., Dershowitz, N., 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":"32_CR4","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proc. 5th Annual ACM Symp. on Theory of Computing, pp. 1\u20139 (1973)","DOI":"10.1145\/800125.804029"},{"issue":"4","key":"32_CR5","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 Communications\u00a022(4), 191\u2013210 (2009)","journal-title":"AI Communications"},{"issue":"1","key":"32_CR6","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H.K. B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified boolean formulas. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"32_CR7","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.\u00a04501, pp. 201\u2013214. Springer, Heidelberg (2007)"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: [38], pp. 28\u201332","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"32_CR9","series-title":"Real-Time Safety Critical Systems Series","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/B978-0-444-89901-9.50012-4","volume-title":"Towards Verified Systems","author":"M.J.C. Gordon","year":"1994","unstructured":"Gordon, M.J.C., Pitts, A.M.: The HOL logic and system. In: Towards Verified Systems. Real-Time Safety Critical Systems Series, vol.\u00a02, pp. 49\u201370. Elsevier, Amsterdam (1994)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"32_CR11","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, language, and interaction: essays in honour of Robin Milner","author":"M. Gordon","year":"2000","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Proof, language, and interaction: essays in honour of Robin Milner, pp. 169\u2013185. MIT Press, Cambridge (2000)"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Bertot, Y.: A short presentation of Coq. In: [38], pp. 12\u201316","DOI":"10.1007\/978-3-540-71067-7_3"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: [38], pp. 33\u201338","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Owre, S., Shankar, N.: A brief overview of PVS. In: [38], pp. 22\u201327","DOI":"10.1007\/978-3-540-71067-7_5"},{"key":"32_CR15","first-page":"170","volume-title":"Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications","author":"R. Kumar","year":"1992","unstructured":"Kumar, R., Kropf, T., Schneider, K.: Integrating a first-order automatic prover in the HOL environment. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pp. 170\u2013176. IEEE Computer Society, Los Alamitos (1992)"},{"key":"32_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-45620-1_10","volume-title":"Automated Deduction - CADE-18","author":"J. Hurd","year":"2002","unstructured":"Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 134\u2013138. Springer, Heidelberg (2002)"},{"issue":"1","key":"32_CR17","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"32_CR18","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T. Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic\u00a07(1), 26\u201340 (2009)","journal-title":"Journal of Applied Logic"},{"key":"32_CR19","unstructured":"Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: A preliminary report. In: 6th International Workshop on Satisfiability Modulo Theories, SMT 2008 (2008)"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3, To appear at the International Conference on Interactive Theorem Proving, ITP-10 (2010)","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"32_CR21","series-title":"Lecture Notes in Artificial Intelligence","first-page":"5","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. 5\u201315. Springer, Heidelberg (2002)"},{"key":"32_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/978-3-642-04222-5_22","volume-title":"FroCos 2009","author":"L. Pulina","year":"2009","unstructured":"Pulina, L., Tacchella, A.: Learning to integrate deduction and search in reasoning about quantified boolean formulas. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 350\u2013365. Springer, Heidelberg (2009)"},{"issue":"1-4","key":"32_CR23","first-page":"145","volume":"2","author":"M. Narizzano","year":"2006","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: Report of the third QBF solvers evaluation. JSAT\u00a02(1-4), 145\u2013164 (2006)","journal-title":"JSAT"},{"key":"32_CR24","unstructured":"Amjad, H.: Combining model checking and theorem proving. Technical Report UCAM-CL-TR-601, University of Cambridge Computer Laboratory, Ph.D. Thesis (2004)"},{"key":"32_CR25","unstructured":"Ballarin, C.: Computer algebra and theorem proving. Technical Report UCAM-CL-TR-473, University of Cambridge Computer Laboratory, Ph.D. Thesis (1999)"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-02614-0_10","volume-title":"Intelligent Computer Mathematics","author":"S. Boldo","year":"2009","unstructured":"Boldo, S., Filli\u00e2tre, J.C., Melquiond, G.: Combining coq and gappa for certifying floating-point programs. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) Calculemus 2009. LNCS, vol.\u00a05625, pp. 59\u201374. Springer, Heidelberg (2009)"},{"key":"32_CR27","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.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"32_CR28","doi-asserted-by":"publisher","first-page":"1047","DOI":"10.1145\/1120725.1120821","volume-title":"Proceedings of the 2005 Conference on Asia South Pacific Design Automation, ASP-DAC 2005","author":"Y. Yu","year":"2005","unstructured":"Yu, Y., Malik, S.: Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In: Tang, T. (ed.) Proceedings of the 2005 Conference on Asia South Pacific Design Automation, ASP-DAC 2005, Shanghai, China, January 18-21, pp. 1047\u20131051. ACM Press, New York (2005)"},{"key":"32_CR29","unstructured":"QDIMACS standard version 1.1 (2005) (released on December 21, 2005), http:\/\/www.qbflib.org\/qdimacs.html (retrieved January 22, 2010)"},{"key":"32_CR30","unstructured":"DIMACS satisfiability suggested format (1993) ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/doc (retrieved January 22, 2010)"},{"key":"32_CR31","unstructured":"Kroening, D., Wintersteiger, C.M.: A file format for QBF certificates (2007), http:\/\/www.verify.ethz.ch\/qbv\/download\/qbcformat.pdf (retrieved September 20, 2009)"},{"key":"32_CR32","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR33","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"key":"32_CR34","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML\u2013 Revised","author":"R. Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML\u2013 Revised. MIT Press, Cambridge (1997)"},{"key":"32_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Barras","year":"2000","unstructured":"Barras, B.: Programming and computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 17\u201337. Springer, Heidelberg (2000)"},{"key":"32_CR36","unstructured":"HOL4 contributors: HOL4 Kananaskis 5 source code (2010), http:\/\/hol.sourceforge.net\/ (retrieved January 22, 2010)"},{"key":"32_CR37","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge (1995), http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/reflect.dvi.gz (retrieved April\u00a08, 2010)"},{"key":"32_CR38","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","year":"2008","unstructured":"Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.): TPHOLs 2008. LNCS, vol.\u00a05170. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,28]],"date-time":"2024-03-28T07:33:19Z","timestamp":1711611199000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}