{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T09:42:14Z","timestamp":1790674934880,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,13]],"date-time":"2015-01-13T00:00:00Z","timestamp":1421107200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P26201"],"award-info":[{"award-number":["P26201"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,1,13]]},"DOI":"10.1145\/2676724.2693176","type":"proceedings-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T13:32:15Z","timestamp":1420464735000},"page":"59-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Certified Connection Tableaux Proofs for HOL Light and TPTP"],"prefix":"10.1145","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[{"name":"University of Innsbruck, Innsbruck, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ji\u0159i","family":"Vysko\u010dil","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Prague, Czech Rep"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,1,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9286-5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881804"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693173"},{"key":"e_1_3_2_1_5_1","first-page":"313","volume-title":"Proceedings of the 13th International Conference on Automated Deduction, number 1104 in LNAI","author":"Harrison J.","year":"1996"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1540610"},{"key":"e_1_3_2_1_7_1","unstructured":"K. Hoder and A. Voronkov . Sine qua non for large theory reasoning . In N. Bj\u00f8rner and V. Sofronie-Stokkermans editors CADE volume 6803 of LNCS pages 299 -- 314 . Springer 2011 . ISBN 978-3-642-22437-9. K. Hoder and A. Voronkov. Sine qua non for large theory reasoning. In N. Bj\u00f8rner and V. Sofronie-Stokkermans editors CADE volume 6803 of LNCS pages 299--314. Springer 2011. ISBN 978-3-642-22437-9."},{"key":"e_1_3_2_1_8_1","first-page":"56","volume-title":"Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA","author":"Hurd J.","year":"2003"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"C. Kaliszyk and J. Urban . Stronger automation for Flyspeck by feature weighting and strategy evolution . In J. C. Blanchette and J. Urban editors PxTP 2013 volume 14 of EPiC Series pages 87 -- 95 . EasyChair 2013. C. Kaliszyk and J. Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In J. C. Blanchette and J. Urban editors PxTP 2013 volume 14 of EPiC Series pages 87--95. EasyChair 2013.","DOI":"10.29007\/5gzr"},{"key":"e_1_3_2_1_10_1","volume-title":"MizAR 40 for Mizar 40. CoRR, abs\/1310.2805","author":"Kaliszyk C.","year":"2013"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_18"},{"key":"e_1_3_2_1_12_1","first-page":"10","article-title":"Learning-assisted theorem proving with millions of lemmas","author":"Kaliszyk C.","year":"2014","journal-title":"J. Symbolic Computation"},{"key":"e_1_3_2_1_13_1","first-page":"10","article-title":"HOL(y)Hammer: Online ATP service for HOL Light","author":"Kaliszyk C.","year":"2014","journal-title":"Mathematics in Computer Science"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9303-3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"C. Kaliszyk L. Mamane and J. Urban . Machine learning of Coq proof guidance: First experiments . In T. Kutsia and A. Voronkov editors SCSS 2014 volume 30 of EPiC Series pages 27 -- 34 . EasyChair 2014. C. Kaliszyk L. Mamane and J. Urban. Machine learning of Coq proof guidance: First experiments. In T. Kutsia and A. Voronkov editors SCSS 2014 volume 30 of EPiC Series pages 27--34. EasyChair 2014.","DOI":"10.29007\/lmmg"},{"key":"e_1_3_2_1_16_1","unstructured":"L. Kov\u00e1cs and A. Voronkov . First-order theorem proving and Vampire . In N. Sharygina and H. Veith editors CAV volume 8044 of LNCS pages 1 -- 35 . Springer 2013 . ISBN 978-3-642-39798-1. L. Kov\u00e1cs and A. Voronkov. First-order theorem proving and Vampire. In N. Sharygina and H. Veith editors CAV volume 8044 of LNCS pages 1--35. Springer 2013. ISBN 978-3-642-39798-1."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_30"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_6"},{"key":"e_1_3_2_1_19_1","first-page":"2015","volume-title":"Model elimination and connection tableau procedures. IncitetDBLP:books\/el\/RobinsonV01","author":"Letz R."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/321450.321456"},{"key":"e_1_3_2_1_21_1","volume-title":"http:\/\/www.cs.unm.edu\/ mccune\/prover9\/","author":"McCune W.","year":"2005"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005843632307"},{"key":"e_1_3_2_1_23_1","first-page":"335","volume-title":"Computing small clause normal forms. IncitetDBLP:books\/el\/RobinsonV01","author":"Nonnengart A."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_19"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1735921.1735931"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(03)00037-3"},{"key":"e_1_3_2_1_27_1","first-page":"23","volume-title":"Automated reasoning and its applications","author":"Paulson L. C.","year":"1997"},{"issue":"3","key":"e_1_3_2_1_28_1","first-page":"73","article-title":"A generic tableau prover and its integration with Isabelle","volume":"5","author":"Paulson L. C.","year":"1999","journal-title":"J. UCS"},{"key":"e_1_3_2_1_29_1","volume-title":"8th IWIL","author":"Paulson L. C.","year":"2010"},{"key":"e_1_3_2_1_30_1","unstructured":"L. C. Paulson and K. W. Susanto . Source-level proof reconstruction for interactive theorem proving . In K. Schneider and J. Brandt editors TPHOLs volume 4732 of LNCS pages 232 -- 245 . Springer 2007 . ISBN 978-3-540-74590-7. L. C. Paulson and K. W. Susanto. Source-level proof reconstruction for interactive theorem proving. In K. Schneider and J. Brandt editors TPHOLs volume 4732 of LNCS pages 232--245. Springer 2007. ISBN 978-3-540-74590-7."},{"key":"e_1_3_2_1_31_1","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"Robinson J. A.","year":"2001"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_49"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00297245"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32211-2_16"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1365980.1365989"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9032-3"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554473.2554486"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1888390.1888429"},{"key":"e_1_3_2_1_39_1","unstructured":"J. Urban J. Vysko\u010dil and P. \u0160t\u011bp\u00e1nek . MaLeCoP: Machine learning connection prover . In K. Br\u00fcnnler and G. Metcalfe editors TABLEAUX volume 6793 of LNCS pages 263 -- 277 . Springer 2011 . ISBN 978-3-642-22118-7. J. Urban J. Vysko\u010dil and P. \u0160t\u011bp\u00e1nek. MaLeCoP: Machine learning connection prover. In K. Br\u00fcnnler and G. Metcalfe editors TABLEAUX volume 6793 of LNCS pages 263--277. Springer 2011. ISBN 978-3-642-22118-7."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9269-y"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753605"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 2015 Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676724.2693176","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676724.2693176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:03Z","timestamp":1750227183000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676724.2693176"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,13]]},"references-count":41,"alternative-id":["10.1145\/2676724.2693176","10.1145\/2676724"],"URL":"https:\/\/doi.org\/10.1145\/2676724.2693176","relation":{},"subject":[],"published":{"date-parts":[[2015,1,13]]},"assertion":[{"value":"2015-01-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}