Cited in
(56)- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Lemma Mining over HOL Light
- Portfolio theorem proving and prover runtime prediction for geometry
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Internal guidance for Satallax
- The role of entropy in guiding a connection prover
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- ENIGMA: efficient learning-based inference guiding machine
- Monte Carlo tableau proof search
- MizarMode
- MPTP
- MPTP 0.2
- MoMM
- MML
- ML4PG
- MaSh
- ileanCoP
- DLog
- leanCoP
- Flyspeck
- PRocH
- MaLARea
- E-MaLeS
- randoCoP
- BliStr
- BliStrTune
- FEMaLeCoP
- SEPIA
- DeepMath
- ENIGMA
- Proofwatch
- TacticToe
- Holophrasm
- Automated and human proofs in general mathematics: an initial comparison
- Overview and evaluation of premise selection techniques for large theory mathematics
- Automated reasoning service for HOL Light
- Theorem proving in large formal mathematics as an emerging AI field
- HOL(y)Hammer: online ATP service for HOL Light
- Efficient Low-Level Connection Tableaux
- Learning-assisted theorem proving with millions of lemmas
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- mizar-items
- Mizar: state-of-the-art and beyond
- NeuroSAT
- ProofWatch: watchlist guidance for large theories in E
- ATPboost: learning premise selection in binary setting with ATP feedback
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- HOList
- Prolog Technology Reinforcement Learning Prover
- Hammering towards QED
- GamePad
- TacticToe: learning to reason with HOL4 tactics
This page was built for software: MaLeCoP
