ENIGMA: efficient learning-based inference guiding machine
From MaRDI portal
Publication:2364687
DOI10.1007/978-3-319-62075-6_20zbMath1367.68249arXiv1701.06532OpenAlexW2581202535WikidataQ62044869 ScholiaQ62044869MaRDI QIDQ2364687
Publication date: 21 July 2017
Full work available at URL: https://arxiv.org/abs/1701.06532
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Make E Smart Again (Short Paper) ⋮ ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) ⋮ Prolog Technology Reinforcement Learning Prover ⋮ Towards finding longer proofs ⋮ The role of entropy in guiding a connection prover ⋮ Learning theorem proving components ⋮ CoProver: a recommender system for proof construction ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ Machine learning guidance for connection tableaux ⋮ Towards the automatic mathematician ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- MaLeS: a framework for automatic tuning of automated theorem provers
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- IeanCOP: lean connection-based theorem proving
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- MaLeCoP Machine Learning Connection Prover
- SEPIA: Search for Proofs Using Inferred Automata
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- The 8th IJCAR automated theorem proving system competition – CASC-J8
- Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction
This page was built for publication: ENIGMA: efficient learning-based inference guiding machine
