MaLeCoP
From MaRDI portal
Software:19250
swMATH7197MaRDI QIDQ19250FDOQ19250
Author name not available (Why is that?)
Cited In (28)
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
- 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
- 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
- Efficient Low-Level Connection Tableaux
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted theorem proving with millions of lemmas
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Mizar: state-of-the-art and beyond
- Prolog Technology Reinforcement Learning Prover
- ProofWatch: watchlist guidance for large theories in E
- ATPboost: learning premise selection in binary setting with ATP feedback
- Hammering towards QED
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- TacticToe: learning to reason with HOL4 tactics
This page was built for software: MaLeCoP
