Proof-pattern recognition and lemma discovery in ACL2

DOI10.1007/978-3-642-45221-5_27MaRDI QIDQ2870142zbMATH OpenOpenAlexFDO

Authors Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1308.1780

zbMATH Keywords

analogylemma discoverypattern recognitionstatistical machine learningtheorem proving

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Pattern recognition, speech recognition (68T10)

Abstract: We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.

Recommendations

• Lemma discovery for induction. A survey
• scientific article; zbMATH DE number 6528605
• Recycling proof patterns in Coq: case studies
• Automatic Learning of Proof Methods in Proof Planning
• Machine Learning for Inductive Theorem Proving

Cited in

(18)

• Formal proofs about rewriting using ACL2
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Lemma discovery for induction. A survey
• Proof mining with dependent types
• Equivalence checking of two functional programs using inductive theorem provers
• ML4PG in computer algebra verification
• A combinator language for theorem discovery
• A learning-based fact selector for Isabelle/HOL
• Recycling proof patterns in Coq: case studies
• Hipster: integrating theory exploration in a proof assistant
• Mining state-based models from proof corpora
• Machine Learning for Inductive Theorem Proving
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• Proof Guidance in PVS with Sequential Pattern Mining
• ACL2(ml): machine-learning for ACL2
• Conjectures, tests and proofs: an overview of theory exploration
• Automating Event-B invariant proofs by rippling and proof patching
• Proof-carrying neuro-symbolic code

Describes a project that uses

Uses Software

• ACL2
• ML4PG
• MaLARea
• HR

This page was built for publication: Proof-pattern recognition and lemma discovery in ACL2

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