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)

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

Describes a project that uses

Uses Software

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

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)