ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
From MaRDI portal
Publication:5049022
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
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)