MizAR 40 for Mizar 40 (Q286800): 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 @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2892718
@@ Property / cites work: Q2892718 / 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 @@
+Sine Qua Non for Large Theory Reasoning
@@ Property / cites work: Sine Qua Non for Large Theory Reasoning / 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 @@
+PRocH: Proof Reconstruction for HOL Light
@@ Property / cites work: PRocH: Proof Reconstruction for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+Lemmatization for Stronger Reasoning in Large Theories
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+MaSh: Machine Learning for Sledgehammer
@@ Property / cites work: MaSh: Machine Learning for Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2755103
@@ Property / cites work: Q2755103 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4413895
@@ Property / cites work: Q4413895 / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+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