Random Forests for Premise Selection

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

Mathematics Subject Classification ID

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

• MPTP
• VAMPIRE
• TPTP
• HOL Light
• Sledgehammer
• MaSh
• E Theorem Prover
• Flyspeck
• HOLyHammer

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