MaSh: Machine Learning for Sledgehammer
From MaRDI portal
Publication:5327335
DOI10.1007/978-3-642-39634-2_6zbMath1317.68215OpenAlexW62264973WikidataQ108482178 ScholiaQ108482178MaRDI QIDQ5327335
Daniel Kühlwein, Josef Urban, Jasmin Christian Blanchette, Cezary Kaliszyk
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.278.3581
Related Items
Proof mining with dependent types, MizAR 40 for Mizar 40, Semi-intelligible Isar proofs from machine-generated proofs, Formalizing Physics: Automation, Presentation and Foundation Issues, System Description: E.T. 0.1, A learning-based fact selector for Isabelle/HOL, Machine Learning for Inductive Theorem Proving, CoProver: a recommender system for proof construction, Random Forests for Premise Selection, Lemmatization for Stronger Reasoning in Large Theories, Learning-assisted theorem proving with millions of lemmas, Machine learning guidance for connection tableaux, Reliable reconstruction of fine-grained proofs in a proof assistant, Hipster: Integrating Theory Exploration in a Proof Assistant, Mining State-Based Models from Proof Corpora, Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
Uses Software
