Learning search control-knowledge for equational deduction
From MaRDI portal
Recommendations
Cited in
(16)- Automatic acquisition of search control knowledge from multiple proof attempts.
- Neural precedence recommender
- Improving ENIGMA-style clause selection while learning from history
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- A connectionist approach for learning search-control heuristics for automated deduction systems (Thesis, TU München, 1997)
- Internal guidance for Satallax
- Lemmatization for stronger reasoning in large theories
- scientific article; zbMATH DE number 1552520 (Why is no real title available?)
- scientific article; zbMATH DE number 1737186 (Why is no real title available?)
- Well-behaved search and the Robbins problem
- Experiments in the heuristic use of past proof experience
- scientific article; zbMATH DE number 1882060 (Why is no real title available?)
- Learning-assisted theorem proving with millions of lemmas
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Automatic acquisition of search guiding heuristics
- Vampire with a brain is a good ITP hammer
This page was built for publication: Learning search control-knowledge for equational deduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2739546)
