swMATH27551MaRDI QIDQ39267FDOQ39267
Author name not available (Why is that?)
Official website: https://arxiv.org/abs/1606.04442
Cited In (38)
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Vampire with a brain is a good ITP hammer
- A neurally-guided, parallel theorem prover
- GamePad
- NeuroSAT
- A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs
- Improving stateful premise selection with transformers
- Improving ENIGMA-style clause selection while learning from history
- The role of entropy in guiding a connection prover
- Machine learning guidance for connection tableaux
- Deepalgebra -- an outline of a program
- Machine learning for mathematical software
- The role of the Mizar mathematical library for interactive proof development in Mizar
- IMLI
- MPTP 0.2
- ML4PG
- MaLeCoP
- MaSh
- FEMaLeCoP
- SEPIA
- kFOIL
- Theoryguru
- OpenNMT
- ATPboost
- ENIGMA
- Proofwatch
- TacticToe
- Holophrasm
- MachSMT
- mizar-items
- nFOIL
- lazyCoP
- MedleySolver
- HOList
- A plugin to export Coq libraries to XML
- Hammer for Coq: automation for dependent type theory
- ProofWatch: watchlist guidance for large theories in E
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
This page was built for software: DeepMath
