swMATH28655MaRDI QIDQ40369FDOQ40369
Author name not available (Why is that?)
Official website: https://link.springer.com/chapter/10.1007%2F978-3-319-62075-6_20
Cited In (61)
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Lash
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Guiding an automated theorem prover with neural rewriting
- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
- A neurally-guided, parallel theorem prover
- GamePad
- NeuroSAT
- Learning to solve geometric construction problems from images
- Online machine learning techniques for Coq: a comparison
- Improving ENIGMA-style clause selection while learning from history
- ENIGMAWatch: ProofWatch meets ENIGMA
- Learning theorem proving components
- The role of entropy in guiding a connection prover
- Towards finding longer proofs
- Machine learning guidance for connection tableaux
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- First neural conjecturing datasets and experiments
- ENIGMA: efficient learning-based inference guiding machine
- MPTP 0.2
- ML4PG
- MaLeCoP
- MaSh
- ileanCoP
- ForTheL
- DLog
- leanCoP
- MaLARea
- randoCoP
- SigmaKEE
- Tactician
- BliStrTune
- FEMaLeCoP
- nanoCoP
- SEPIA
- ProofTool
- kFOIL
- SUMO
- DeepMath
- ATPboost
- MadMax
- Proofwatch
- TacticToe
- Twee
- Holophrasm
- CoDe
- GKC
- TreeRePair
- MurmurHash
- Neural precedence recommender
- ACER
- nFOIL
- lazyCoP
- HOList
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Make E Smart Again (Short Paper)
- Prolog Technology Reinforcement Learning Prover
- ProofWatch: watchlist guidance for large theories in E
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Euclidea
This page was built for software: ENIGMA
