swMATH8206MaRDI QIDQ20216FDOQ20216
Author name not available (Why is that?)
Official website: http://www4.in.tum.de/~blanchet/mash.pdf
Cited In (43)
- A neurally-guided, parallel theorem prover
- Lemma Mining over HOL Light
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Semi-intelligible Isar proofs from machine-generated proofs
- Mining state-based models from proof corpora
- Random forests for premise selection
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Title not available (Why is that?)
- Machine learning guidance for connection tableaux
- Proof mining with dependent types
- Machine learning for mathematical software
- ML4PG
- MaLeCoP
- ForTheL
- Dr.Doodle
- Flyspeck
- PRocH
- MaLARea
- HOLyHammer
- E-MaLeS
- BliStr
- MizAR 40 for Mizar 40
- System description: E.T. 0.1
- A learning-based fact selector for Isabelle/HOL
- Openproof
- Speedith
- SEPIA
- SRASS
- Theoryguru
- DeepMath
- Holophrasm
- Regular_Algebras
- MaSh: machine learning for Sledgehammer
- Hybrid computation
- Lemmatization for stronger reasoning in large theories
- Learning-assisted theorem proving with millions of lemmas
- Inspection and selection of representations
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Formalizing physics: automation, presentation and foundation issues
- ML4PG in computer algebra verification
- Hipster: integrating theory exploration in a proof assistant
- Hammering towards QED
This page was built for software: MaSh
