Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448): Difference between revisions

@@ label / en / label / en @@
+Hammering Mizar by Learning Clause Guidance (Short Paper).
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+A learning-based fact selector for Isabelle/HOL
@@ Property / cites work: A learning-based fact selector for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering towards QED
@@ Property / cites work: Hammering towards QED / rank @@
+Normal rank
@@ Property / cites work @@
+Q3096176
@@ Property / cites work: Q3096176 / rank @@
+Normal rank
@@ Property / cites work @@
+Random Forests for Premise Selection
@@ Property / cites work: Random Forests for Premise Selection / rank @@
+Normal rank
@@ Property / cites work @@
+Monte Carlo tableau proof search
@@ Property / cites work: Monte Carlo tableau proof search / rank @@
+Normal rank
@@ Property / cites work @@
+TacticToe: Learning to Reason with HOL4 Tactics
@@ Property / cites work: TacticToe: Learning to Reason with HOL4 Tactics / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMAWatch: ProofWatch meets ENIGMA
@@ Property / cites work: ENIGMAWatch: ProofWatch meets ENIGMA / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+SEPIA: Search for Proofs Using Inferred Automata
@@ Property / cites work: SEPIA: Search for Proofs Using Inferred Automata / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA: efficient learning-based inference guiding machine
+Normal rank
@@ Property / cites work @@
+Enhancing ENIGMA given clause guidance
@@ Property / cites work: Enhancing ENIGMA given clause guidance / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+Lemmatization for Stronger Reasoning in Large Theories
+Normal rank
@@ Property / cites work @@
+Deep Network Guided Proof Search
@@ Property / cites work: Deep Network Guided Proof Search / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E 1.8
@@ Property / cites work: System Description: E 1.8 / rank @@
+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 @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaLeCoP
@@ Property / describes a project that uses: MaLeCoP / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2977777155
@@ Property / OpenAlex ID: W2977777155 / rank @@
+Normal rank
@@ Property / title @@
+Hammering Mizar by Learning Clause Guidance (Short Paper). (English)
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5875448