Learning Proof Transformations and Its Applications in Interactive Theorem Proving

DOI10.1007/978-3-031-43369-6_13MaRDI QIDQ6496633zbMATH OpenFDO

Authors Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban

Publication date 3 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43369-6_13

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• TacticToe: learning to prove with tactics
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• TacticToe: learning to reason with HOL4 tactics
• CoProver: a recommender system for proof construction
• Machine Learning for Inductive Theorem Proving

Cites work

• A Brief Overview of HOL4
• Aligning concepts across proof assistant libraries
• Automating formalization by statistical and semantic parsing of mathematics
• ENIGMA: efficient learning-based inference guiding machine
• First neural conjecturing datasets and experiments
• scientific article; zbMATH DE number 1179314 (Why is no real title available?)
• scientific article; zbMATH DE number 7015112 (Why is no real title available?)
• scientific article; zbMATH DE number 7178362 (Why is no real title available?)
• scientific article; zbMATH DE number 3349328 (Why is no real title available?)
• scientific article; zbMATH DE number 3412190 (Why is no real title available?)
• Internal guidance for Satallax
• Mizar: state-of-the-art and beyond
• Online machine learning techniques for Coq: a comparison
• Premise selection for mathematics by corpus analysis and kernel methods
• Random forests
• SEPIA: search for proofs using inferred automata
• TacticToe: learning to prove with tactics
• The Lean theorem prover (system description)
• The role of the Mizar mathematical library for interactive proof development in Mizar
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• Vampire with a brain is a good ITP hammer

Cited in

(3)

• TacticToe: learning to prove with tactics
• CoProver: a recommender system for proof construction
• Learning guided automated reasoning: a brief survey

This page was built for publication: Learning Proof Transformations and Its Applications in Interactive Theorem Proving

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