Internal Guidance for Satallax

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• VAMPIRE
• Satallax
• Sledgehammer
• PicoSAT
• MaLeCoP
• leanCoP
• ileanCoP
• Flyspeck
• Easychair
• FEMaLeCoP
• kepler98

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