ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
From MaRDI portal
Publication:5049022
DOI10.1007/978-3-030-51054-1_29OpenAlexW3038615574MaRDI QIDQ5049022FDOQ5049022
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
Cites Work
- MizAR 40 for Mizar 40
- LIBLINEAR: a library for large linear classification
- MPTP 0.2: Design, implementation, and initial experiments
- MaLARea
- Title not available (Why is that?)
- Hammer for Coq: automation for dependent type theory
- Enhancing ENIGMA given clause guidance
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- A learning-based fact selector for Isabelle/HOL
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Learning search control-knowledge for equational deduction
- Title not available (Why is that?)
- A New Class of Automated Theorem-Proving Algorithms
- Aligning concepts across proof assistant libraries
- ENIGMAWatch: ProofWatch meets ENIGMA
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- ENIGMA: efficient learning-based inference guiding machine
- Fingerprint indexing for paramodulation and rewriting
- Sharing HOL4 and HOL Light proof knowledge
- Hammering towards QED
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
Cited In (16)
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
- Learning to solve geometric construction problems from images
- Improving ENIGMA-style clause selection while learning from history
- Learning theorem proving components
- The role of entropy in guiding a connection prover
- Towards finding longer proofs
- Learning from Łukasiewicz and Meredith: investigations into proof structures
- Neural precedence recommender
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
- Invariant neural architecture for learning term synthesis in instantiation proving
- Investigations into proof structures
- Translating SUMO-K to Higher-Order Set Theory
- Bulldozer: A Cribless Rapid Analytical Machine (RAM) Solution to Enigma and its Variations
- VizAR: visualization of automated reasoning proofs (system description)
Uses Software
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)
