Hammering Mizar by Learning Clause Guidance (Short Paper).
From MaRDI portal
Publication:5875448
DOI10.4230/LIPIcs.ITP.2019.34OpenAlexW2977777155MaRDI QIDQ5875448
Publication date: 3 February 2023
Full work available at URL: https://arxiv.org/abs/1904.01677
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Vampire with a brain is a good ITP hammer ⋮ Alien coding ⋮ Improving ENIGMA-style clause selection while learning from history
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Flyspeck
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- MPTP 0.2: Design, implementation, and initial experiments
- Enhancing ENIGMA given clause guidance
- ENIGMAWatch: ProofWatch meets ENIGMA
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- ENIGMA: efficient learning-based inference guiding machine
- Monte Carlo tableau proof search
- System Description: E 1.8
- Random Forests for Premise Selection
- Lemmatization for Stronger Reasoning in Large Theories
- 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
- Deep Network Guided Proof Search
- TacticToe: Learning to Reason with HOL4 Tactics
- Hammering towards QED
This page was built for publication: Hammering Mizar by Learning Clause Guidance (Short Paper).
