Learning-assisted theorem proving with millions of lemmas (Q485842): Difference between revisions

@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+Automated and Human Proofs in General Mathematics: An Initial Comparison
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT Solvers
@@ Property / cites work: Extending Sledgehammer with SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Recording and analysing knowledge-based distributed deduction processes
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+Optimizing proof search in model elimination
@@ Property / cites work: Optimizing proof search in model elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Sine Qua Non for Large Theory Reasoning
@@ Property / cites work: Sine Qua Non for Large Theory Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning Service for HOL Light
@@ Property / cites work: Automated Reasoning Service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Lemma Mining over HOL Light
@@ Property / cites work: Lemma Mining over HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+PRocH: Proof Reconstruction for HOL Light
@@ Property / cites work: PRocH: Proof Reconstruction for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+HOL(y)Hammer: online ATP service for HOL Light
@@ Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+MaSh: Machine Learning for Sledgehammer
@@ Property / cites work: MaSh: Machine Learning for Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+E-MaLeS 1.1
@@ Property / cites work: E-MaLeS 1.1 / rank @@
+Normal rank
@@ Property / cites work @@
+Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Q2739546
@@ Property / cites work: Q2739546 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+SRASS - A Semantic Relevance Axiom Selection System
+Normal rank
@@ Property / cites work @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Large Formal Mathematics as an Emerging AI Field
+Normal rank
@@ Property / cites work @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Using hints to increase the effectiveness of an automated reasoning program: Case studies
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Q3829089
@@ Property / cites work: Q3829089 / rank @@
+Normal rank