Improving ENIGMA-style clause selection while learning from history

DOI10.1007/978-3-030-79876-5_31OpenAlexW3186348969MaRDI QIDQ2055886

Martin Suda

Publication date: 1 December 2021

Full work available at URL: https://arxiv.org/abs/2102.13564

zbMATH Keywords

machine learningrecursive neural networksclause selectionsaturation-based theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Vampire with a brain is a good ITP hammer

Uses Software

• SMT-LIB
• SPASS
• DeepMath
• ENIGMA
• MobileNetV2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Limited resource strategy in resolution theorem proving
• Enhancing ENIGMA given clause guidance
• 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
• ENIGMA: efficient learning-based inference guiding machine
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• AVATAR: The Architecture for First-Order Theorem Provers
• Playing with AVATAR
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Deep Network Guided Proof Search
• Learning domain knowledge to improve theorem proving
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Coming to terms with quantified reasoning
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Verification, Model Checking, and Abstract Interpretation