{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:14:35Z","timestamp":1760015675048,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Wallenberg Academy Fellowship 2014"},{"name":"EPSRC grant Reasoning in Verification and Security"},{"name":"Swedish VR grant","award":["D049770 GenPro"],"award-info":[{"award-number":["D049770 GenPro"]}]},{"name":"Austrian FWF National Re- search Network RiSE","award":["S11409-N23"],"award-info":[{"award-number":["S11409-N23"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854071","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T13:18:57Z","timestamp":1452604737000},"page":"37-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["The vampire and the FOOL"],"prefix":"10.1145","author":[{"given":"Evgenii","family":"Kotelnikov","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Sweden"}]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[{"name":"University of Manchester, UK"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[{"name":"University of Manchester, UK \/ Chalmers University of Technology, Sweden \/ EasyChair, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Department of Computer Science","author":"Barrett C.","year":"2010","unstructured":"C. Barrett , A. Stump , and C. Tinelli . The SMT-LIB Standard: Version 2.0. Technical report , Department of Computer Science , The University of Iowa , 2010 . Available at www.SMT-LIB.org. C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010. Available at www.SMT-LIB.org."},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"177","volume-title":"Proc. of CAV","author":"Barrett C.","year":"2011","unstructured":"C. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . CVC4 . In Proc. of CAV , volume 6806 of LNCS , pages 171\u2013 177 , 2011 . C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proc. of CAV, volume 6806 of LNCS, pages 171\u2013177, 2011."},{"key":"e_1_3_2_1_3_1","series-title":"LNCS","first-page":"294","volume-title":"Proc. of CADE","author":"Baumgartner P.","year":"2015","unstructured":"P. Baumgartner . SMTtoTPTP \u2014 a converter for theorem proving formats . In Proc. of CADE , volume 9195 of LNCS , pages 285\u2013 294 , 2015 . P. Baumgartner. SMTtoTPTP \u2014 a converter for theorem proving formats. In Proc. of CADE, volume 9195 of LNCS, pages 285\u2013294, 2015."},{"key":"e_1_3_2_1_4_1","series-title":"LNAI","first-page":"170","volume-title":"Proc. of IJCAR","author":"Benzm\u00fcller C.","year":"2008","unstructured":"C. Benzm\u00fcller , L. Paulson , F. Theiss , and A. Fietzke . LEO-II \u2014 A Cooperative Automatic Theorem Prover for Higher-Order Logic . In Proc. of IJCAR , volume 5195 of LNAI , pages 162\u2013 170 , 2008 . C. Benzm\u00fcller, L. Paulson, F. Theiss, and A. Fietzke. LEO-II \u2014 A Cooperative Automatic Theorem Prover for Higher-Order Logic. In Proc. of IJCAR, volume 5195 of LNAI, pages 162\u2013170, 2008."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_29"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"340","volume-title":"Proc. of TACAS","author":"de Moura L. M.","year":"2008","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: an efficient SMT solver . In Proc. of TACAS , volume 4963 of LNCS , pages 337\u2013 340 , 2008 . L. M. de Moura and N. Bj\u00f8rner. Z3: an efficient SMT solver. In Proc. of TACAS, volume 4963 of LNCS, pages 337\u2013340, 2008."},{"key":"e_1_3_2_1_8_1","first-page":"185","volume":"8837","author":"Gupta A.","year":"2014","unstructured":"A. Gupta , L. Kov\u00e1cs , B. Kragl , and A. Voronkov . Extensionality Crisis and Proving Identity. In Proc. of ATVA , volume 8837 of LNCS, pages 185 \u2013 200 , 2014 . A. Gupta, L. Kov\u00e1cs, B. Kragl, and A. Voronkov. Extensionality Crisis and Proving Identity. In Proc. of ATVA, volume 8837 of LNCS, pages 185\u2013200, 2014.","journal-title":"Extensionality Crisis and Proving Identity. In Proc. of ATVA"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554473.2554477"},{"key":"e_1_3_2_1_10_1","series-title":"LNCS","first-page":"86","volume-title":"Proc. of CICM","author":"Kotelnikov E.","year":"2015","unstructured":"E. Kotelnikov , L. Kov\u00e1cs , and A. Voronkov . A First Class Boolean Sort in First-Order Theorem Proving and TPTP . In Proc. of CICM , volume 9150 of LNCS , pages 71\u2013 86 , 2015 . E. Kotelnikov, L. Kov\u00e1cs, and A. Voronkov. A First Class Boolean Sort in First-Order Theorem Proving and TPTP. In Proc. of CICM, volume 9150 of LNCS, pages 71\u201386, 2015."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958033"},{"key":"e_1_3_2_1_13_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer , 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002."},{"key":"e_1_3_2_1_14_1","series-title":"LNCS","first-page":"213","volume-title":"Proc. of CADE","author":"Reynolds A.","year":"2015","unstructured":"A. Reynolds and J. Blanchette . A Decision Procedure for (Co)datatypes in SMT Solvers . In Proc. of CADE , volume 9195 of LNCS , pages 197\u2013 213 , 2015 . A. Reynolds and J. Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. In Proc. of CADE, volume 9195 of LNCS, pages 197\u2013213, 2015."},{"key":"e_1_3_2_1_15_1","series-title":"LNCS","first-page":"743","volume-title":"Proc. of LPAR","author":"Schulz S.","year":"2013","unstructured":"S. Schulz . System Description: E 1.8 . In Proc. of LPAR , volume 8312 of LNCS , pages 735\u2013 743 , 2013 . S. Schulz. System Description: E 1.8. In Proc. of LPAR, volume 8312 of LNCS, pages 735\u2013743, 2013."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9143-8"},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the CADE-25 ATP System Competition CASC-25. Technical report","author":"Sutcliffe G.","year":"2015","unstructured":"G. Sutcliffe . Proceedings of the CADE-25 ATP System Competition CASC-25. Technical report , University of Miami , US, 2015 . http:\/\/www.cs.miami.edu\/~tptp\/CASC\/25\/Proceedings.pdf. G. Sutcliffe. Proceedings of the CADE-25 ATP System Competition CASC-25. Technical report, University of Miami, US, 2015. http:\/\/www.cs.miami.edu\/~tptp\/CASC\/25\/Proceedings.pdf."},{"issue":"1","key":"e_1_3_2_1_18_1","first-page":"1","volume":"3","author":"Sutcliffe G.","year":"2010","unstructured":"G. Sutcliffe and C. Benzm\u00fcller . Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning , 3 ( 1 ): 1 \u2013 27 , 2010 . G. Sutcliffe and C. Benzm\u00fcller. Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning, 3 (1):1\u201327, 2010.","journal-title":"J. Formalized Reasoning"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_32"}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854071","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854071","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:46Z","timestamp":1750225726000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":19,"alternative-id":["10.1145\/2854065.2854071","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854071","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}