ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)

DOI10.1007/978-3-030-51054-1_29OpenAlexW3038615574MaRDI QIDQ5049022

Miroslav Olšák, Karel Chvalovský, Bartosz Piotrowski, Jan Jakubův, Martin Suda, Josef Urban

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

neural networksdecision treesmachine learningautomated theorem provingsaturation-style proving

Mathematics Subject Classification ID

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

Related Items (11)

Learning to solve geometric construction problems from images ⋮ Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Towards finding longer proofs ⋮ The role of entropy in guiding a connection prover ⋮ Learning theorem proving components ⋮ VizAR: visualization of automated reasoning proofs (system description) ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures ⋮ Neural precedence recommender ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• MPTP 0.2
• VAMPIRE
• LIBLINEAR
• E Theorem Prover
• Flyspeck
• MaLARea
• HOLyHammer
• TensorFlow
• XGBoost
• ENIGMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MaLARea
• MizAR 40 for Mizar 40
• A learning-based fact selector for Isabelle/HOL
• MPTP 0.2: Design, implementation, and initial experiments
• Aligning concepts across proof assistant libraries
• Hammer for Coq: automation for dependent type theory
• Enhancing ENIGMA given clause guidance
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• HOL(y)Hammer: online ATP service for HOL Light
• ENIGMAWatch: ProofWatch meets ENIGMA
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• ENIGMA: efficient learning-based inference guiding machine
• Fingerprint Indexing for Paramodulation and Rewriting
• Sharing HOL4 and HOL Light Proof Knowledge
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• A New Class of Automated Theorem-Proving Algorithms
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Hammering towards QED

This page was built for publication: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)