Random Forests for Premise Selection
From MaRDI portal
Publication:2964471
DOI10.1007/978-3-319-24246-0_20zbMath1471.68307OpenAlexW2296462965WikidataQ108482160 ScholiaQ108482160MaRDI QIDQ2964471
Michael Färber, Cezary Kaliszyk
Publication date: 27 February 2017
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_20
Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
Online machine learning techniques for Coq: a comparison ⋮ Vampire with a brain is a good ITP hammer ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Hammer for Coq: automation for dependent type theory ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper).
Uses Software
Cites Work
- Bagging predictors
- MizAR 40 for Mizar 40
- MPTP-motivation, implementation, first experiments
- Theoretical comparison between the Gini Index and Information Gain criteria
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- System Description: E 1.8
- A Brief Overview of Mizar
- Extending Sledgehammer with SMT Solvers
- Sine Qua Non for Large Theory Reasoning
- MaSh: Machine Learning for Sledgehammer
- Random forests
This page was built for publication: Random Forests for Premise Selection
