ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
From MaRDI portal
Publication:5049022
Cites work
- A learning-based fact selector for Isabelle/HOL
- A New Class of Automated Theorem-Proving Algorithms
- Aligning concepts across proof assistant libraries
- Enhancing ENIGMA given clause guidance
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- ENIGMA: efficient learning-based inference guiding machine
- ENIGMAWatch: ProofWatch meets ENIGMA
- Fingerprint indexing for paramodulation and rewriting
- Hammer for Coq: automation for dependent type theory
- Hammering towards QED
- HOL(y)Hammer: online ATP service for HOL Light
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1882060 (Why is no real title available?)
- Learning search control-knowledge for equational deduction
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- LIBLINEAR: a library for large linear classification
- MaLARea
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- MizAR 40 for Mizar 40
- MPTP 0.2: Design, implementation, and initial experiments
- 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
(22)- Learning from Łukasiewicz and Meredith: investigations into proof structures
- Neural precedence recommender
- Improving ENIGMA-style clause selection while learning from history
- Learning to solve geometric construction problems from images
- Towards finding longer proofs
- The role of entropy in guiding a connection prover
- Learning theorem proving components
- Bulldozer: A Cribless Rapid Analytical Machine (RAM) Solution to Enigma and its Variations
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- VizAR: visualization of automated reasoning proofs (system description)
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
- Translating SUMO-K to Higher-Order Set Theory
- Invariant neural architecture for learning term synthesis in instantiation proving
- Investigations into proof structures
- When GNNs met a word equations solver: learning to rank equations
- Efficient neural clause-selection reinforcement
- Machine learning for quantifier selection in cvc5
- How much should this symbol weigh? A GNN-advised clause selection
- Learning guided automated reasoning: a brief survey
- An empirical assessment of progress in automated theorem proving
- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
Describes a project that uses
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)
