Random forests for premise selection
From MaRDI portal
Recommendations
- Premise selection for mathematics by corpus analysis and kernel methods
- Overview and evaluation of premise selection techniques for large theory mathematics
- Improving stateful premise selection with transformers
- Machine learning for first-order theorem proving
- ATPboost: learning premise selection in binary setting with ATP feedback
Cites work
- A Brief Overview of Mizar
- Bagging predictors
- Extending Sledgehammer with SMT solvers
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- MPTP-motivation, implementation, first experiments
- MaSh: machine learning for Sledgehammer
- MizAR 40 for Mizar 40
- Premise selection for mathematics by corpus analysis and kernel methods
- Random forests
- Sine qua non for large theory reasoning
- System description: E 1.8
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Theoretical comparison between the Gini Index and Information Gain criteria
Cited in
(12)- Vampire with a brain is a good ITP hammer
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Random forests and selected samples
- Portfolio theorem proving and prover runtime prediction for geometry
- Improving stateful premise selection with transformers
- Online machine learning techniques for Coq: a comparison
- Learning guided automated reasoning: a brief survey
- Premise selection in the Naproche system
- Overview and evaluation of premise selection techniques for large theory mathematics
- Graph sequence learning for premise selection
- Hammer for Coq: automation for dependent type theory
- ATPboost: learning premise selection in binary setting with ATP feedback
Describes a project that uses
Uses Software
This page was built for publication: Random forests for premise selection
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964471)
