Proof-Pattern Recognition and Lemma Discovery in ACL2

J. Heras, E. Komendantskaya, M. Johansson, E. Maclean

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages18
ISBN (Electronic)978-3-642-45221-5
ISBN (Print)978-3-642-45220-8
Publication statusPublished - 1 Aug 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Keywords / Materials (for Non-textual outputs)

  • Computer Science - Logic in Computer Science


Dive into the research topics of 'Proof-Pattern Recognition and Lemma Discovery in ACL2'. Together they form a unique fingerprint.

Cite this