Improving ENIGMA-style clause selection while learning from history
From MaRDI portal
Recommendations
Cites work
- Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
- AVATAR: The Architecture for First-Order Theorem Provers
- Coming to terms with quantified reasoning
- Deep learning
- Deep network guided proof search
- Enhancing ENIGMA given clause guidance
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- ENIGMA: efficient learning-based inference guiding machine
- Faster, higher, stronger: E 2.3
- GKC: a reasoning system for large knowledge bases
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- scientific article; zbMATH DE number 6378127 (Why is no real title available?)
- Intrinsic volumes and mixed volumes
- Layered clause selection for theory reasoning (short paper)
- Learning domain knowledge to improve theorem proving
- Learning search control-knowledge for equational deduction
- Limited resource strategy in resolution theorem proving
- Paramodulation-based theorem proving
- Performance of clause selection heuristics for saturation-based theorem proving
- Playing with AVATAR
- Property invariant embedding for automated reasoning
- Resolution theorem proving
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Verification, Model Checking, and Abstract Interpretation
Cited in
(11)- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)
- Solving hard Mizar problems with instantiation and strategy invention
- Invariant neural architecture for learning term synthesis in instantiation proving
- When GNNs met a word equations solver: learning to rank equations
- Context-aware clause selection using symbol name meanings in theorem proving
- Efficient neural clause-selection reinforcement
- How much should this symbol weigh? A GNN-advised clause selection
- Learning guided automated reasoning: a brief survey
- Vampire with a brain is a good ITP hammer
This page was built for publication: Improving ENIGMA-style clause selection while learning from history
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055886)
