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

DOI10.1007/978-3-030-51054-1_29MaRDI QIDQ5049022zbMATH OpenOpenAlexFDO

Authors Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, 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

machine learningdecision treesneural networksautomated theorem provingsaturation-style proving

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1882060 (Why is no real title available?)
• A New Class of Automated Theorem-Proving Algorithms
• A learning-based fact selector for Isabelle/HOL
• Aligning concepts across proof assistant libraries
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA: efficient learning-based inference guiding machine
• ENIGMAWatch: ProofWatch meets ENIGMA
• Enhancing ENIGMA given clause guidance
• Fingerprint indexing for paramodulation and rewriting
• HOL(y)Hammer: online ATP service for HOL Light
• Hammer for Coq: automation for dependent type theory
• Hammering towards QED
• LIBLINEAR: a library for large linear classification
• Learning search control-knowledge for equational deduction
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• MPTP 0.2: Design, implementation, and initial experiments
• MaLARea
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• MizAR 40 for Mizar 40
• Sharing HOL4 and HOL Light proof knowledge
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Using hints to increase the effectiveness of an automated reasoning program: Case studies

Cited in

(16)

• Learning theorem proving components
• The role of entropy in guiding a connection prover
• Towards finding longer proofs
• Investigations into proof structures
• Fast and slow enigmas and parental guidance
• Vampire with a brain is a good ITP hammer
• Bulldozer: A Cribless Rapid Analytical Machine (RAM) Solution to Enigma and its Variations
• Translating SUMO-K to Higher-Order Set Theory
• Neural precedence recommender
• Fully reusing clause deduction algorithm based on standard contradiction separation rule
• Improving ENIGMA-style clause selection while learning from history
• Invariant neural architecture for learning term synthesis in instantiation proving
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• Learning to solve geometric construction problems from images
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• VizAR: visualization of automated reasoning proofs (system description)

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5049022)