Proof-Pattern Recognition and Lemma Discovery in ACL2

DOI10.1007/978-3-642-45221-5_27zbMath1407.68436arXiv1308.1780OpenAlexW1549265610MaRDI QIDQ2870142

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

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

pattern recognitiontheorem provinganalogylemma discoverystatistical machine learning

Mathematics Subject Classification ID

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

Related Items

Proof mining with dependent types, A learning-based fact selector for Isabelle/HOL, Equivalence checking of two functional programs using inductive theorem provers, Machine Learning for Inductive Theorem Proving, Recycling proof patterns in Coq: case studies, Automating Event-B invariant proofs by rippling and proof patching, Hipster: Integrating Theory Exploration in a Proof Assistant, Mining State-Based Models from Proof Corpora

Uses Software

• ACL2
• ML4PG
• MaLARea
• HR