ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414): Difference between revisions

@@ 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 @@
+MPTP 0.2
@@ Property / describes a project that uses: MPTP 0.2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+E Theorem Prover
@@ Property / describes a project that uses: E Theorem Prover / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+XGBoost
@@ Property / describes a project that uses: XGBoost / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaLeCoP
@@ Property / describes a project that uses: MaLeCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+leanCoP
@@ Property / describes a project that uses: leanCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaLARea
@@ Property / describes a project that uses: MaLARea / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FEMaLeCoP
@@ Property / describes a project that uses: FEMaLeCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BliStr
@@ Property / describes a project that uses: BliStr / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LIBLINEAR
@@ Property / describes a project that uses: LIBLINEAR / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BliStrTune
@@ Property / describes a project that uses: BliStrTune / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ATPboost
@@ Property / describes a project that uses: ATPboost / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Proofwatch
@@ Property / describes a project that uses: Proofwatch / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ENIGMA
@@ Property / describes a project that uses: ENIGMA / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2969934262
@@ Property / OpenAlex ID: W2969934262 / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+Mizar: State-of-the-art and Beyond
@@ Property / cites work: Mizar: State-of-the-art and Beyond / rank @@
+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 @@
+Machine learning for first-order theorem proving
@@ Property / cites work: Machine learning for first-order theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Q3096176
@@ Property / cites work: Q3096176 / rank @@
+Normal rank
@@ Property / cites work @@
+Internal Guidance for Satallax
@@ Property / cites work: Internal Guidance for Satallax / 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 @@
+ProofWatch: watchlist guidance for large theories in E
+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 @@
+Hierarchical invention of theorem proving strategies
+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 @@
+Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
+Normal rank
@@ Property / cites work @@
+Deep Network Guided Proof Search
@@ Property / cites work: Deep Network Guided Proof Search / rank @@
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 -- July 2, 2016. Proceedings
+Normal rank
@@ Property / cites work @@
+IeanCOP: lean connection-based theorem proving
@@ Property / cites work: IeanCOP: lean connection-based theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+A New Class of Automated Theorem-Proving Algorithms
+Normal rank
@@ Property / cites work @@
+ATPboost: learning premise selection in binary setting with ATP feedback
+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 @@
+Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
+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