MaSh: machine learning for Sledgehammer

DOI10.1007/978-3-642-39634-2_6MaRDI QIDQ5327335zbMATH OpenOpenAlexWikidataFDO

Authors Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban

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

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05)

Recommendations

• A learning-based fact selector for Isabelle/HOL
• Sledgehammer: judgement day
• TacticToe: learning to reason with HOL4 tactics
• Machine learning for first-order theorem proving
• Learning-assisted theorem proving with millions of lemmas

Cited in

(24)

• Machine learning guidance for connection tableaux
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Online machine learning techniques for Coq: a comparison
• Simple dataset for proof method recommendation in Isabelle/HOL
• Proof mining with dependent types
• MizAR 40 for Mizar 40
• Semi-intelligible Isar proofs from machine-generated proofs
• Random forests for premise selection
• Lemmatization for stronger reasoning in large theories
• A learning-based fact selector for Isabelle/HOL
• Formalizing physics: automation, presentation and foundation issues
• System description: E.T. 0.1
• TacticToe: learning to reason with HOL4 tactics
• Learning-assisted theorem proving with millions of lemmas
• Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
• Hipster: integrating theory exploration in a proof assistant
• Mining state-based models from proof corpora
• Sledgehammer: judgement day
• Machine Learning for Inductive Theorem Proving
• CoProver: a recommender system for proof construction
• Graph sequence learning for premise selection
• Learning guided automated reasoning: a brief survey
• Lemma discovery and strategies for automated induction
• The Naproche-ZF theorem prover (short paper)

Describes a project that uses

Uses Software

• Isabelle/HOL
• Mizar
• Sledgehammer
• MaSh
• HOL Light

This page was built for publication: MaSh: machine learning for Sledgehammer

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327335)