We are also grateful to the anonymous reviewers for their many suggestions and comments ,
Sledgehammer research was supported by the Deutsche Forschungsgemeinschaft projects Quis Custodiet (grants NI 491/11-1 and NI 491/11-2) and Hardening the Hammer (grant NI 491/14-1) Kaliszyk is supported by the Austrian Science Fund (FWF) grant P26201. Sledgehammer was originally supported by the UK's Engineering and Physical Sciences Research Council ,
Integrating Automated and Interactive Theorem Proving, Automated Deduction?A Basis for Applications, volume II: Systems and Implementation Techniques, pp.97-116, 1998. ,
DOI : 10.1007/978-94-017-0435-9_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.4447
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods, Journal of Automated Reasoning, vol.50, issue.1???2, pp.191-213, 2014. ,
DOI : 10.1007/s10817-013-9286-5
Automated and Human Proofs in General Mathematics: An Initial Comparison, Bjørner and Voronkov, pp.37-45 ,
DOI : 10.1007/978-3-642-28717-6_6
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar, Intelligent Computer Mathematics LNCS, vol.7362, pp.1-16, 2012. ,
DOI : 10.1007/978-3-642-31374-5_1
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Jouannaud and Shao [74], pp.135-150 ,
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130
Armin Fiedler, Helmut Horacek, and Quoc Bao Vo. Assertion-level proof representation with under-specification ,
The mutilated chessboard problem?checked by Mizar, pp.43-46 ,
Verification of clock synchronization algorithms: experiments on a combination of deductive tools, Formal Aspects of Computing, vol.144, issue.2, pp.321-341, 2007. ,
DOI : 10.1007/s00165-007-0027-6
URL : https://hal.archives-ouvertes.fr/inria-00097383
Mathematical Induction in Otter-Lambda, Journal of Automated Reasoning, vol.5, issue.2, pp.311-344, 2006. ,
DOI : 10.1007/s10817-006-9036-z
OTTER Proofs in Tarskian Geometry, Demri et al. [53], pp.495-510 ,
DOI : 10.1007/978-3-319-08587-6_38
On computer-assisted proofs in ordinal number theory, J. Autom. Reason, vol.22, issue.2, pp.341-378, 1999. ,
LEO-II?A cooperative automatic theorem prover for classical higherorder logic (system description), Armando et al. [7], pp.162-170 ,
Automatic proof construction in type theory using resolution, J. Autom. Reason, vol.29, pp.3-4253, 2002. ,
Redirecting proofs by contradiction, pp.11-26 ,
Semi-intelligible Isar proofs from machinegenerated proofs ,
Encoding monomorphic and polymorphic types, Tools and Algorithms for the Construction and Analysis of Systems, pp.493-507, 2013. ,
Monotonicity Inference for Higher-Order Formulas, Journal of Automated Reasoning, vol.178, issue.1, pp.369-398, 2011. ,
DOI : 10.1007/s10817-011-9234-1
More SPASS with Isabelle?Superposition with hard sorts and configurable simplification, Interactive Theorem Proving, pp.345-360, 2012. ,
Latent Dirichlet allocation, J. Mach. Learn. Res, vol.3, pp.993-1022, 2003. ,
Reconstruction of Z3???s Bit-Vector Proofs in HOL4 and Isabelle/HOL, Jouannaud and Shao [74], pp.183-198 ,
DOI : 10.1016/j.jal.2007.07.003
Sledgehammer: Judgement Day, Giesl and Hähnle, pp.107-121 ,
DOI : 10.1007/978-3-642-14203-1_9
Fast LCF-Style Proof Reconstruction for Z3, Interactive Theorem Proving, pp.179-194, 2010. ,
DOI : 10.1007/978-3-642-14052-5_14
Using reflection to build efficient and certified decision procedures, Theoretical Aspects of Computer Software (TACS '97), volume 1281 of LNCS, pp.515-529 ,
DOI : 10.1007/BFb0014565
Machine Learning for First-Order Theorem Proving, Journal of Automated Reasoning, vol.32, issue.12, pp.141-172, 2014. ,
DOI : 10.1007/s10817-014-9301-5
Satallax: An Automatic Higher-Order Prover, Gramlich et al. [65], pp.111-117 ,
DOI : 10.1007/978-3-642-31365-3_11
Informalising formal mathematics: Searching the Mizar library with latent semantics, Asperti et al. [8], pp.58-72 ,
The SNoW learning architecture, 1999. ,
A TLA + proof system, LPAR 2008 Workshops CEUR Workshop Proceedings. CEUR-WS.org, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00338299
Personalized recommendation on dynamic content using predictive bilinear models, Proceedings of the 18th international conference on World wide web, WWW '09, pp.691-700, 2009. ,
DOI : 10.1145/1526709.1526802
Sort It Out with Monotonicity, Bjørner and Sofronie-Stokkermans [18], pp.207-221 ,
DOI : 10.1007/BF00243005
New techniques that improve MACEstyle finite model finding, Model Computation?Principles, 2003. ,
Comparison of SVM and Some Older Classification Algorithms in Text Classification Tasks, Artificial Intelligence in Theory and Practice IFIP International Federation for Information Processing, pp.169-178, 2006. ,
DOI : 10.1007/978-0-387-34747-9_18
The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts, Controlled Natural Language, pp.170-186, 2009. ,
DOI : 10.1007/978-3-642-14418-9_11
Premise Selection in the Naproche System, Giesl and Hähnle [63], pp.434-440 ,
DOI : 10.1007/978-3-642-14203-1_37
C-CoRN, the Constructive Coq Repository at Nijmegen, Asperti et al. [8], pp.88-103 ,
DOI : 10.1007/3-540-45620-1_12
Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem, Journal of Algebra, vol.208, issue.2, pp.526-532, 1998. ,
DOI : 10.1006/jabr.1998.7467
Integration of automated and interactive theorem proving in ILP, Conference on Automated Deduction (CADE-14), volume 1249 of LNCS, pp.57-60, 1997. ,
Interpretation of a Mizar-like logic in first-order logic Automated Deduction in Classical and Non-Classical Logics, LNCS, vol.1761, pp.137-151, 2000. ,
Experiments with random projection, Uncertainty in Artificial Intelligence (UAI '00), pp.143-151, 2000. ,
Obvious logical inferences, International Joint Conference on Artificial Intelligence (IJCAI '81), pp.530-531, 1981. ,
Indexing by latent semantic analysis, J ,
Learning from previous proof experience, 1999. ,
The distance-weighted k-nearest-neighbor rule, IEEE Trans. Syst. Man Cybern., SMC, vol.6, issue.4, pp.325-327, 1976. ,
Using Yices as an automated solver in Isabelle/HOL, Automated Formal Methods (AFM '08), pp.3-13, 2008. ,
Why3 ??? Where Programs Meet Provers, European Symposium on Programming, pp.125-128, 2013. ,
DOI : 10.1007/978-3-642-37036-6_8
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, Tools and Algorithms for the Construction and Analysis of Systems, pp.167-181, 2006. ,
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088
Integrating an Automated Theorem Prover into Agda, NASA Formal Methods, pp.116-130, 2011. ,
DOI : 10.1007/978-3-540-70594-9_15
Regular algebras Archive of Formal Proofs, 2014. ,
Matching Concepts across HOL Libraries, Conference on Intelligent Computer Mathematics, pp.267-281, 2014. ,
DOI : 10.1007/978-3-319-08434-3_20
URL : http://arxiv.org/abs/1405.3906
Premise Selection and External Provers for HOL4, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.49-57, 2015. ,
DOI : 10.1145/2676724.2693173
A Machine-Checked Proof of the Odd Order Theorem, Blazy et al. [26], pp.163-179 ,
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699
Developments in formal proofs. CoRR, abs/1408, pp.2013-2014, 1086. ,
Optimizing proof search in model elimination, Conference on Automated Deduction (CADE-13), pp.313-327, 1996. ,
DOI : 10.1007/3-540-61511-3_97
Sine Qua Non for Large Theory Reasoning, Bjørner and Sofronie-Stokkermans [18], pp.299-314 ,
DOI : 10.1007/978-3-642-15582-6_30
Translating machine-generated resolution proofs into NDproofs at the assertion level, Pacific Rim International Conference on Artificial Intelligence (PRICAI '96), pp.399-410, 1996. ,
Integrating Gandalf and HOL, Theorem Proving in Higher Order Logics (TPHOLs '99), volume 1690 of LNCS, pp.311-321, 1999. ,
DOI : 10.1007/3-540-48256-3_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.7221
First-order proof tactics in higher-order logic theorem provers, Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pp.56-68, 2003. ,
A STATISTICAL INTERPRETATION OF TERM SPECIFICITY AND ITS APPLICATION IN RETRIEVAL, Journal of Documentation, vol.28, issue.1, pp.11-21, 1972. ,
DOI : 10.1108/eb026526
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems, ACL2 Theorem Prover and its Applications of Electronic Proceedings in Theoretical Computer Science, pp.77-85, 2014. ,
DOI : 10.4204/EPTCS.152.6
Machine learning of Coq proof guidance: First experiments, Symbolic Computation in Software Science, pp.27-34, 2014. ,
System Description: E.T. 0.1, Conference on Automated Deduction, 2015. ,
DOI : 10.1007/978-3-319-21401-6_27
MizAR 40 for Mizar 40, Journal of Automated Reasoning, vol.50, issue.1-2, 2013. ,
DOI : 10.1007/s10817-015-9330-8
PRocH: Proof Reconstruction for HOL Light, Bonacina [31], pp.267-274 ,
DOI : 10.1007/978-3-642-38574-2_18
Stronger automation for Flyspeck by feature weighting and strategy evolution, pp.87-95 ,
Learning-Assisted Automated Reasoning with Flyspeck, Journal of Automated Reasoning, vol.50, issue.1???2, pp.173-213, 2014. ,
DOI : 10.1007/s10817-014-9303-3
HOL(y)Hammer: Online ATP Service for HOL Light, Mathematics in Computer Science, vol.50, issue.1, pp.5-22, 2015. ,
DOI : 10.1007/s11786-014-0182-0
Learning-assisted theorem proving with millions of lemmas, Journal of Symbolic Computation, vol.69, pp.109-128, 2015. ,
DOI : 10.1016/j.jsc.2014.09.032
Machine Learner for Automated Reasoning 0.4 and 0.5. CoRR, abs, 1402. ,
MaSh: Machine Learning for Sledgehammer, pp.35-50 ,
DOI : 10.1007/978-3-642-39634-2_6
E-MaLeS 1.1, Bonacina [31], pp.407-413 ,
DOI : 10.1007/978-3-642-38574-2_28
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics, Gramlich et al. [65], pp.378-392 ,
DOI : 10.1007/978-3-642-31365-3_30
Integrating a firstorder automatic prover in the HOL environment, Myla Archer ,
Evidence algorithm and system for automated deduction: A retrospective view, pp.411-426 ,
Verification of executable pipelined machines with bit-level interfaces, ICCAD-2005. IEEE/ACM International Conference on Computer-Aided Design, 2005., pp.855-862, 2005. ,
DOI : 10.1109/ICCAD.2005.1560182
The mutilated checkerboard in set theory, pp.25-26 ,
Solution of the Robbins problem, Journal of Automated Reasoning, vol.19, issue.3, pp.263-276, 1997. ,
DOI : 10.1023/A:1005843212881
Mace4 Reference Manual and Guide, 2003. ,
DOI : 10.2172/822574
Ivy: A Preprocessor and Proof Checker for First-Order Logic, Computer-Aided Reasoning: ACL2 Case Studies, number 4 in Advances in Formal Methods, pp.265-282, 2000. ,
DOI : 10.1007/978-1-4757-3188-0_16
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, pp.43-51, 2006. ,
DOI : 10.1016/j.entcs.2005.12.005
Metamath, 1997. ,
DOI : 10.1007/11542384_13
System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level, Conference on Automated Deduction (CADE-17), volume 1831 of LNCS, pp.460-464, 2000. ,
DOI : 10.1007/10721959_37
Translating Higher-Order Clauses to First-Order Clauses, Journal of Automated Reasoning, vol.9, issue.2, pp.35-60, 2008. ,
DOI : 10.1007/s10817-007-9085-y
Lightweight relevance filtering for machine-generated resolution problems, Journal of Applied Logic, vol.7, issue.1, pp.41-57, 2009. ,
DOI : 10.1016/j.jal.2007.07.004
Automatic Verification of TLA???+??? Proof Obligations with SMT Solvers, Bjørner and Voronkov [19], pp.289-303 ,
DOI : 10.1007/978-3-642-28717-6_23
URL : https://hal.archives-ouvertes.fr/hal-00760570
Efficient estimation of word representations in vector space, 1301. ,
An integration of resolution and natural deduction theorem proving, National Conference on Artificial Intelligence (AAAI-86), volume I. Science, pp.198-202, 1986. ,
leanCoP: lean connection-based theorem proving, Journal of Symbolic Computation, vol.36, issue.1-2, pp.139-161, 2003. ,
DOI : 10.1016/S0747-7171(03)00037-3
A generic tableau prover and its integration with Isabelle, J. Univers. Comput. Sci, vol.5, issue.3, pp.73-87, 1999. ,
A simple formalization and proof for the mutilated chess board, Log. J. IGPL, vol.9, issue.3, pp.499-509, 2001. ,
Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, International Workshop on the Implementation of Logics, pp.1-11, 2010. ,
Source-level proof reconstruction for interactive theorem proving, Theorem Proving in Higher Order Logics, pp.232-245, 2007. ,
First order reasoning on a large ontology, pp.61-70 ,
Analytic and non-analytic proofs, Conference on Automated Deduction, pp.394-413, 1984. ,
DOI : 10.1007/978-0-387-34768-4_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.3237
Automated theorem proving in quasigroup and loop theory, AI Commun, vol.23, issue.2-3, pp.267-283, 2010. ,
The methods of improving and reorganizing natural deduction proofs, Mathematical User Interfaces (MathUI10), 2010. ,
Improving legibility of natural deduction proofs is not trivial, Logical Methods in Computer Science, vol.10, issue.3, p.2014 ,
DOI : 10.2168/LMCS-10(3:23)2014
Ensemble based systems in decision making, IEEE Circuits and Systems Magazine, vol.6, issue.3, pp.21-45, 2006. ,
DOI : 10.1109/MCAS.2006.1688199
Semantic selection of premisses for automated theorem proving, pp.27-44 ,
Automated Development of Fundamental Mathematical Theories, Kluwer, 1992. ,
Software framework for topic modelling with large corpora, New Challenges for NLP Frameworks 2010, pp.45-50, 2010. ,
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering, Conference on Automated Deduction (CADE-22), pp.157-162, 2009. ,
DOI : 10.1007/978-3-540-71070-7_37
Obvious inferences, Journal of Automated Reasoning, vol.3, issue.4, pp.383-393, 1987. ,
DOI : 10.1007/BF00247436
Tutorial: Automated Formal Methods with PVS, SAL, and Yices, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), p.262, 2006. ,
DOI : 10.1109/SEFM.2006.37
Learning Search Control Knowledge for Equational Deduction, DISKI. Infix, vol.230, 2000. ,
First-order deduction for large knowledge bases, Deduction at Scale 2011 Seminar, 2011. ,
Rank Aggregation for Similar Items, SIAM International Conference on Data Mining (SDM07), pp.587-592, 2007. ,
DOI : 10.1137/1.9781611972771.66
Proof Development with ???mega: The Irrationality of $$\sqrt 2$$, Thirty Five Years of Automating Mathematics, pp.271-314, 2003. ,
DOI : 10.1007/978-94-017-0253-9_11
SCOTT: Semantically constrained otter system description, Bundy [36], pp.764-768 ,
DOI : 10.1007/3-540-58156-1_56
System description: An interface between CLAM and HOL, Conference on Automated Deduction (CADE-15), volume 1421 of LNCS, pp.134-138, 1998. ,
DOI : 10.1007/BFb0054255
Robust, semiintelligible Isabelle proofs from ATP proofs, pp.117-132 ,
SEMANTIC DERIVATION VERIFICATION: TECHNIQUES AND IMPLEMENTATION, International Journal on Artificial Intelligence Tools, vol.15, issue.06, pp.1053-1070, 2006. ,
DOI : 10.1142/S0218213006003119
The TPTP World ??? Infrastructure for Automated Reasoning, Logic for Programming , Artificial Intelligence, and Reasoning (LPAR-16), pp.1-12, 2010. ,
DOI : 10.1007/978-3-642-17511-4_1
Empirically Successful Automated Reasoning in Large Theories, CEUR Workshop Proceedings. CEUR-WS.org, 2007. ,
MPTP ? Motivation, Implementation, First Experiments, Journal of Automated Reasoning, vol.21, issue.2, pp.319-339, 2004. ,
DOI : 10.1007/s10817-004-6245-1
MizarMode???an integrated proof assistance tool for the Mizar way of formalizing mathematics, Journal of Applied Logic, vol.4, issue.4, pp.414-427, 2006. ,
DOI : 10.1016/j.jal.2005.10.004
MoMM ??? FAST INTERREDUCTION AND RETRIEVAL IN LARGE LIBRARIES OF FORMALIZED MATHEMATICS, International Journal on Artificial Intelligence Tools, vol.15, issue.01, pp.109-130, 2006. ,
DOI : 10.1142/S0218213006002588
MPTP 0.2: Design, Implementation, and Initial Experiments, Journal of Automated Reasoning, vol.15, issue.1, pp.21-43, 2006. ,
DOI : 10.1007/s10817-006-9032-3
Making semantic processing and presentation of MML easy, Mathematical Knowledge Management (MKM 2005), pp.346-360, 2006. ,
MaLARea: A metasystem for automated reasoning in large theories, pp.45-58 ,
Content-based encoding of mathematical and code libraries, Proceedings of the ITP 2011 Workshop on Mathematical Wikis (MathWikis), number 767 in CEUR Workshop Proceedings, pp.49-53, 2011. ,
BliStr: The Blind Strategymaker. CoRR, abs, 1301. ,
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library, International Congress on Mathematical Software, pp.155-166, 2010. ,
DOI : 10.1007/978-3-642-15582-6_30
ATP and Presentation Service for Mizar Formalizations, Journal of Automated Reasoning, vol.2, issue.2, pp.229-241, 2013. ,
DOI : 10.1007/s10817-012-9269-y
URL : http://arxiv.org/abs/1109.0616
ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments, Mathematics in Computer Science, vol.2, issue.2, pp.231-251, 2008. ,
DOI : 10.1007/s11786-008-0053-7
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar, pp.132-146 ,
DOI : 10.1007/978-3-642-14128-7_12
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance, Armando et al. [7], pp.441-456 ,
DOI : 10.1007/978-3-540-71070-7_37
Combining Mizar and TPTP semantic presentation and verification tools, Studies in Logic, Grammar and Rhetoric, pp.121-136, 2009. ,
DOI : 10.1007/11618027_23
MaLeCoP Machine Learning Connection Prover, Automated Reasoning with Analytic Tableaux and Related Methods, pp.263-277, 2011. ,
DOI : 10.1007/s10817-006-9032-3
URL : http://repository.ubn.ru.nl/bitstream/2066/92021/1/92021.pdf
System for Automated Deduction (SAD): A Tool for Proof Verification, Conference on Automated Deduction (CADE-21), pp.398-403, 2007. ,
DOI : 10.1007/978-3-540-73595-3_29
Using hints to increase the effectiveness of an automated reasoning program: Case studies, Journal of Automated Reasoning, vol.29, issue.3, pp.223-239, 1996. ,
DOI : 10.1007/BF00252178
SMT solvers: new oracles for the HOL theorem prover, International Journal on Software Tools for Technology Transfer, vol.7, issue.1, pp.419-429, 2011. ,
DOI : 10.1007/s10009-011-0188-8
Combining Superposition, Sorts and Splitting, Handbook of Automated Reasoning, pp.1965-2013, 2001. ,
DOI : 10.1016/B978-044450813-3/50029-1
URL : http://hdl.handle.net/11858/00-001M-0000-000F-31F3-8
Integrated proof transformation services, Computer-Supported Mathematical Theory Development, pp.33-48, 2004. ,