Internal Guidance for Satallax
From MaRDI portal
Publication:2817934
DOI10.1007/978-3-319-40229-1_24zbMath1475.68435arXiv1605.09293OpenAlexW2414651070MaRDI QIDQ2817934
Michael Färber, Chad Edward Brown
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1605.09293
Related Items
Portfolio theorem proving and prover runtime prediction for geometry ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Extending SMT solvers to higher-order logic ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Lash 1.0 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- LEO-II and Satallax on the Sledgehammer test bench
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- System Description: E 1.8
- Satallax: An Automatic Higher-Order Prover
- MaLeCoP Machine Learning Connection Prover
- System Description: E.T. 0.1
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Sine Qua Non for Large Theory Reasoning