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