{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:56Z","timestamp":1776333416692,"version":"3.51.2"},"reference-count":75,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,2,27]],"date-time":"2018-02-27T00:00:00Z","timestamp":1519689600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["714034"],"award-info":[{"award-number":["714034"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9458-4","type":"journal-article","created":{"date-parts":[[2018,2,27]],"date-time":"2018-02-27T02:16:00Z","timestamp":1519697760000},"page":"423-453","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":87,"title":["Hammer for Coq: Automation for Dependent Type Theory"],"prefix":"10.1007","volume":"61","author":[{"given":"\u0141ukasz","family":"Czajka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,27]]},"reference":[{"key":"9458_CR1","unstructured":"Alemi, A.A., Chollet, F., Irving, G., Szegedy, C., Urban, J.: DeepMath\u2014Deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., Luxburg, U.V., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems (NIPS 2016), pp. 2235\u20132243 (2016)"},{"key":"9458_CR2","first-page":"285","volume-title":"Frontiers of Combining Systems (FroCoS 2005), Volume 3717 of LNCS","author":"A Abel","year":"2005","unstructured":"Abel, A., Coquand, T., Norell, U.: Connecting a logical framework to a first-order logic prover. In: Gramlich, B. (ed.) Frontiers of Combining Systems (FroCoS 2005), Volume 3717 of LNCS, pp. 285\u2013301. Springer, New York (2005)"},{"key":"9458_CR3","first-page":"135","volume-title":"Certified Programs and Proofs (CPP 2011), Volume 7086 of LNCS","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011), Volume 7086 of LNCS, pp. 135\u2013150. Springer, New York (2011)"},{"issue":"2","key":"9458_CR4","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9458_CR5","first-page":"91","volume":"7","author":"A Asperti","year":"2014","unstructured":"Asperti, A., Ricciotti, W., Coen, CSacerdoti: Matita tutorial. J. Formaliz. Reason. 7(2), 91\u2013199 (2014)","journal-title":"J. Formaliz. Reason."},{"key":"9458_CR6","doi-asserted-by":"crossref","unstructured":"Aspinall, D.: Proof general: a generic tool for proof development. In: Graf, S., Schwartzbach, M.I. (eds.) Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, volume 1785 of LNCS, pp. 38\u201342. Springer, New York (2000)","DOI":"10.1007\/3-540-46419-0_3"},{"key":"9458_CR7","first-page":"146","volume-title":"Mathematical Knowledge Management (MKM 2007), Volume 4573 of LNCS","author":"A Asperti","year":"2007","unstructured":"Asperti, A., Tassi, E.: Higher order proof reconstruction from paramodulation-based refutations: the unit equality case. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Mathematical Knowledge Management (MKM 2007), Volume 4573 of LNCS, pp. 146\u2013160. Springer, New York (2007)"},{"key":"9458_CR8","unstructured":"Asperti, A., Tassi, E.: Smart matching. In: Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5\u201310, 2010. Proceedings, pp. 263\u2013277 (2010)"},{"key":"9458_CR9","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. (2015)","DOI":"10.1007\/s10817-015-9335-3"},{"key":"9458_CR10","unstructured":"Bancerek, G., Byli\u0144ski, C., Grabowski, A. Korni\u0142owicz, A., Matuszewski, R., Naumowicz, A., P\u0105k, K., Urban, J.: Mizar: State-of-the-art and beyond. In: Intelligent Computer Mathematics\u2014International Conference, CICM 2015, Washington, DC, USA, July 13\u201317, 2015, Proceedings, pp. 261\u2013279 (2015)"},{"key":"9458_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, New York (2004)"},{"issue":"3","key":"9458_CR12","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1093\/logcom\/exi016","volume":"15","author":"S Broda","year":"2005","unstructured":"Broda, S., Damas, L.: On long normal inhabitants of a type. J. Log. Comput. 15(3), 353\u2013390 (2005)","journal-title":"J. Log. Comput."},{"key":"9458_CR13","first-page":"73","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2009), Volume 5674 of LNCS","author":"A Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda\u2014A functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009), Volume 5674 of LNCS, pp. 73\u201378. Springer, New York (2009)"},{"key":"9458_CR14","first-page":"12","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2008), Volume 5170 of LNCS","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y.: A short presentation of Coq. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2008), Volume 5170 of LNCS, pp. 12\u201316. Springer, New York (2008)"},{"issue":"3","key":"9458_CR15","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Greenaway, D., Kaliszyk, C., K\u00fchlwein, D., Urban, J.: A learning-based fact selector for Isabelle\/HOL. J. Autom. Reason. 57(3), 219\u2013244 (2016)","journal-title":"J. Autom. Reason."},{"issue":"3\u20134","key":"9458_CR16","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. J. Autom. Reason. 29(3\u20134), 253\u2013275 (2002)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9458_CR17","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"key":"9458_CR18","unstructured":"Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2012). http:\/\/www21.in.tum.de\/~blanchet\/phdthesis.pdf"},{"issue":"5","key":"9458_CR19","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013)","journal-title":"J. Funct. Program."},{"key":"9458_CR20","first-page":"179","volume-title":"Interactive Theorem Proving (ITP 2010), Volume 6172 of LNCS","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) Interactive Theorem Proving (ITP 2010), Volume 6172 of LNCS, pp. 179\u2013194. Springer, New York (2010)"},{"key":"9458_CR21","unstructured":"Ben-Yelles, C.: Type-assignment in the lambda-calculus: syntax and semantics. Ph.D. thesis, Mathematics Department, University of Wales, Swansea, UK (1979)"},{"issue":"2\/3","key":"9458_CR22","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"9458_CR23","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types\u2014A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types\u2014A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"9458_CR24","doi-asserted-by":"crossref","unstructured":"Czajka, \u0141., Kaliszyk, C.: Goal translation for a hammer for Coq (extended abstract). In: Blanchette, J.C., Kaliszyk, C. (eds.) First International Workshop on Hammers for Type Theories (HaTT 2016), Volume 210 of EPTCS, pp. 13\u201320 (2016)","DOI":"10.4204\/EPTCS.210.4"},{"key":"9458_CR25","unstructured":"Coq Development Team: The Coq proof assistant reference manual (2016). Version 8.6"},{"key":"9458_CR26","first-page":"162","volume-title":"Types for Proofs and Programs (TYPES 2003), Volume 3085 of LNCS","author":"P Corbineau","year":"2003","unstructured":"Corbineau, P.: First-order reasoning in the calculus of inductive constructions. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs (TYPES 2003), Volume 3085 of LNCS, pp. 162\u2013177. Springer, New York (2003)"},{"key":"9458_CR27","unstructured":"Czajka, \u0141.: A shallow embedding of pure type systems into first-order logic. Submitted. (2016). http:\/\/www.mimuw.edu.pl\/~lukaszcz\/emb.pdf"},{"key":"9458_CR28","first-page":"337","volume-title":"TACAS 2008, Volume 4963 of LNCS","author":"LM Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008, Volume 4963 of LNCS, pp. 337\u2013340. Springer, New York (2008)"},{"key":"9458_CR29","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover. In: Felty, A.P., Middeldorp, A. (eds.) International Conference on Automated Deduction (CADE 2015), Volume 9195 of LNCS, pp. 378\u2013388. Springer, New York (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"9458_CR30","unstructured":"de\u00a0Moura, L., Selsam, D.: Congruence closure in intensional type theory. In: Olivetti, N., Tiwari, A. (eds.) International Joint Conference on Automated Reasoning, IJCAR 2016, Volume 9706 of LNCS. Springer, New York (2016)"},{"issue":"3","key":"9458_CR31","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","volume":"3","author":"G Dowek","year":"1993","unstructured":"Dowek, G.: A complete proof synthesis method for the cube of type systems. J. Log. Comput. 3(3), 287\u2013315 (1993)","journal-title":"J. Log. Comput."},{"issue":"3","key":"9458_CR32","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log. 57(3), 795\u2013807 (1992)","journal-title":"J. Symb. Log."},{"key":"9458_CR33","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C.: One logic to use them all. In: Bonacina, M.P. (ed.) International Conference on Automated Deduction (CADE 2013), Volume 7898 of LNCS, pp. 1\u201320. Springer, New York (2013)","DOI":"10.1007\/978-3-642-38574-2_1"},{"key":"9458_CR34","doi-asserted-by":"crossref","unstructured":"F\u00e4rber, M., Kaliszyk, C.: Random forests for premise selection. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems (FroCoS 2015), Volume 9322 of LNCS, pp. 325\u2013340 (2015)","DOI":"10.1007\/978-3-319-24246-0_20"},{"key":"9458_CR35","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) European Symposium on Programming (ESOP 2013), Volume 7792 of LNCS, pp. 125\u2013128. Springer, New York (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"9458_CR36","first-page":"163","volume-title":"Interactive Theorem Proving (ITP 2013), Volume 7998 of LNCS","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving (ITP 2013), Volume 7998 of LNCS, pp. 163\u2013179. Springer, New York (2013)"},{"issue":"2","key":"9458_CR37","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formaliz. Reason. 3(2), 95\u2013152 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"9458_CR38","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: The four colour theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM, Volume 5081 of LNCS, pp. 333. Springer, New York (2007)","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"9458_CR39","doi-asserted-by":"crossref","unstructured":"Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) International Conference on Automated Deduction (CADE 2015), Volume 9195 of LNCS, pp. 246\u2013255. Springer, New York (2015)","DOI":"10.1007\/978-3-319-21401-6_16"},{"key":"9458_CR40","first-page":"60","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2009), Volume 5674 of LNCS","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009), Volume 5674 of LNCS, pp. 60\u201366. Springer, New York (2009)"},{"issue":"1","key":"9458_CR41","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1656274.1656278","volume":"11","author":"M Hall","year":"2009","unstructured":"Hall, M., Frank, E., Holmes, G., Pfahringer, B., Reutemann, P., Witten, I.H.: The Weka data mining software: an update. SIGKDD Explor. Newsl. 11(1), 10\u201318 (2009)","journal-title":"SIGKDD Explor. Newsl."},{"key":"9458_CR42","doi-asserted-by":"crossref","unstructured":"Hindley, J.R.: Basic Simple Type Theory, Volume\u00a042 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1997)","DOI":"10.1017\/CBO9780511608865"},{"key":"9458_CR43","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), Number NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"9458_CR44","first-page":"135","volume-title":"Handbook of the History of Logic vol 9 (Computational Logic)","author":"J Harrison","year":"2014","unstructured":"Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Siekmann, J. (ed.) Handbook of the History of Logic vol 9 (Computational Logic), pp. 135\u2013214. Elsevier, Amsterdam (2014)"},{"key":"9458_CR45","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) 23rd International Conference on Automated Deduction (CADE 2011), Volume 6803 of LNCS, pp. 299\u2013314. Springer, New York (2011)","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"9458_CR46","doi-asserted-by":"crossref","unstructured":"Joosten, S., Kaliszyk, C., Urban, J.: Initial experiments with TPTP-style automated theorem provers on ACL2 problems. In: Verbeek, F., Schmaltz, J. (eds.) ACL2 Theorem Prover and Its Applications (ACL2 2014), Volume 152 of EPTCS, pp. 77\u201385 (2014)","DOI":"10.4204\/EPTCS.152.6"},{"key":"9458_CR47","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1108\/eb026526","volume":"28","author":"KS Jones","year":"1972","unstructured":"Jones, K.S.: A statistical interpretation of term specificity and its application in retrieval. J. Doc. 28, 11\u201321 (1972)","journal-title":"J. Doc."},{"key":"9458_CR48","doi-asserted-by":"crossref","unstructured":"Komendantskaya, E. Heras, J., Grov, G.: Machine learning in Proof General: Interfacing interfaces. In: Kaliszyk, C., L\u00fcth, C. (eds.) User Interfaces for Theorem (UITP 2012), Volume 118 of EPTCS, pp. 15\u201341 (2013)","DOI":"10.4204\/EPTCS.118.2"},{"key":"9458_CR49","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C. Mamane, L. Urban, J.: Machine learning of Coq proof guidance: First experiments. In: Kutsia, T., Voronkov, A. (eds.) Symbolic Computation in Software Science (SCSS 2014), Volume\u00a030 of EPiC, pp. 27\u201334. EasyChair (2014)","DOI":"10.29007\/lmmg"},{"key":"9458_CR50","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: PRocH: Proof reconstruction for HOL Light. In: Bonacina, M.P. (ed.) International Conference on Automated Deduction (CADE 2013), Volume 7898 of LNCS, pp. 267\u2013274. Springer, New York (2013)","DOI":"10.1007\/978-3-642-38574-2_18"},{"key":"9458_CR51","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) Proof Exchange for Theorem Proving (PxTP 2013), Volume\u00a014 of EPiC, pp. 87\u201395. EasyChair (2013)","DOI":"10.29007\/5gzr"},{"issue":"2","key":"9458_CR52","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9458_CR53","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"9458_CR54","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109\u2013128 (2015)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"9458_CR55","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015)","journal-title":"J. Autom. Reason."},{"key":"9458_CR56","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 3084\u20133090. AAAI Press, Palo Alto (2015)"},{"key":"9458_CR57","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer-Aided Verification (CAV 2013), Volume 8044 of LNCS, pp. 1\u201335. Springer, New York (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9458_CR58","doi-asserted-by":"crossref","unstructured":"K\u00fchlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) International Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of LNCS, pp. 378\u2013392. Springer, New York (2012)","DOI":"10.1007\/978-3-642-31365-3_30"},{"key":"9458_CR59","unstructured":"Laurent, J.: Suggesting relevant lemmas by learning from successful proofs. Technical report, \u00c9cole normale sup\u00e9rieure (2016). Internship Report"},{"key":"9458_CR60","unstructured":"Letouzey, P.: Programmation fonctionnelle certifi\u00e9e : L\u2019extraction de programmes dans l\u2019assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant). PhD thesis, University of Paris-Sud, Orsay, France, (2004)"},{"issue":"1","key":"9458_CR61","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. J. Autom. Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9458_CR62","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41\u201357 (2009)","journal-title":"J. Appl. Log."},{"key":"9458_CR63","unstructured":"Paulson, L.C., Blanchette, J.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: 8th IWIL (2010)"},{"key":"9458_CR64","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007), Volume 4732 of LNCS, pp. 232\u2013245. Springer, New York (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"9458_CR65","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence (LPAR 2013), Volume 8312 of LNCS, pp. 735\u2013743. Springer, New York (2013)"},{"key":"9458_CR66","doi-asserted-by":"crossref","unstructured":"Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: Jprover : Integrating connection-based theorem proving into interactive proof assistants. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, Volume 2083 of Lecture Notes in Computer Science, pp. 421\u2013426. Springer, New York (2001)","DOI":"10.1007\/3-540-45744-5_34"},{"key":"9458_CR67","first-page":"28","volume-title":"TPHOLs 2008, Volume 5170 of LNCS","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008, Volume 5170 of LNCS, pp. 28\u201332. Springer, New York (2008)"},{"key":"9458_CR68","first-page":"1","volume-title":"LPAR-16, Number 6355 in LNAI","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP world-infrastructure for automated reasoning. In: Clarke, E., Voronkov, A. (eds.) LPAR-16, Number 6355 in LNAI, pp. 1\u201312. Springer, New York (2010)"},{"issue":"6","key":"9458_CR69","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1093\/logcom\/8.6.713","volume":"8","author":"T Tammet","year":"1998","unstructured":"Tammet, T., Smith, J.M.: Optimized encodings of fragments of type theory in first-order logic. J. Log. Comput. 8(6), 713\u2013744 (1998)","journal-title":"J. Log. Comput."},{"issue":"3\u20134","key":"9458_CR70","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J Urban","year":"2004","unstructured":"Urban, J.: MPTP\u2014motivation, implementation. First Exp. J. Autom. Reason. 33(3\u20134), 319\u2013339 (2004)","journal-title":"First Exp. J. Autom. Reason."},{"issue":"5","key":"9458_CR71","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1007\/s11225-016-9661-4","volume":"104","author":"P Urzyczyn","year":"2016","unstructured":"Urzyczyn, P.: Intuitionistic games: determinacy, completeness, and normalization. Stud. Log. 104(5), 957\u20131001 (2016)","journal-title":"Stud. Log."},{"key":"9458_CR72","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) Intelligent Computer Mathematics (CICM 2010), Volume 6167 of LNCS, pp. 132\u2013146 (2010)","DOI":"10.1007\/978-3-642-14128-7_12"},{"key":"9458_CR73","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Mizar\u2019s soft type system. In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10\u201313, 2007, Proceedings, pp. 383\u2013399 (2007)","DOI":"10.1007\/978-3-540-74591-4_28"},{"key":"9458_CR74","first-page":"33","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2008), Volume 5170 of LNCS","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2008), Volume 5170 of LNCS, pp. 33\u201338. Springer, New York (2008)"},{"key":"9458_CR75","doi-asserted-by":"crossref","unstructured":"Zielenkiewicz, M., Schubert, A.: Automata theory approach to predicate intuitionistic logic. In: Logic-Based Program Synthesis and Transformation\u201426th International Symposium, LOPSTR 2016, Revised Selected Papers, pp. 345\u2013360 (2016)","DOI":"10.1007\/978-3-319-63139-4_20"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9458-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9458-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9458-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T01:16:30Z","timestamp":1751418990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9458-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,27]]},"references-count":75,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9458"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9458-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,27]]},"assertion":[{"value":"30 March 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}