Vampire with a brain is a good ITP hammer
From MaRDI portal
Publication:831938
DOI10.1007/978-3-030-86205-3_11OpenAlexW3202844695MaRDI QIDQ831938
Publication date: 24 March 2022
Full work available at URL: https://arxiv.org/abs/2102.03529
Uses Software
Cites Work
- MizAR 40 for Mizar 40
- MPTP 0.2: Design, implementation, and initial experiments
- Limited resource strategy in resolution theorem proving
- Enhancing ENIGMA given clause guidance
- Improving ENIGMA-style clause selection while learning from history
- Layered clause selection for theory reasoning (short paper)
- Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Faster, higher, stronger: E 2.3
- GKC: a reasoning system for large knowledge bases
- Premise selection for mathematics by corpus analysis and kernel methods
- ENIGMA: efficient learning-based inference guiding machine
- Monte Carlo tableau proof search
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- AVATAR: The Architecture for First-Order Theorem Provers
- Random Forests for Premise Selection
- MaLeCoP Machine Learning Connection Prover
- Playing with AVATAR
- Deep Network Guided Proof Search
- Learning domain knowledge to improve theorem proving
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Hammering towards QED
- Sine Qua Non for Large Theory Reasoning
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Vampire with a brain is a good ITP hammer
