Proof-pattern recognition and lemma discovery in ACL2

Jonathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean

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

    18 Citations (Scopus)

    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.
    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
    EditorsKen McMIllan, Aart Middledorp, Andrei Voronkov
    Place of PublicationBerlin
    PublisherSpringer
    Pages389-406
    Number of pages18
    ISBN (Electronic)9783642452215
    ISBN (Print)9783642452208
    DOIs
    Publication statusPublished - 2013
    Event19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Stellenbosch, South Africa
    Duration: 14 Dec 201319 Dec 2013
    http://www.cs.sun.ac.za/lpar-19/

    Publication series

    NameLecture notes in computer science
    PublisherSpringer
    Volume8312

    Conference

    Conference19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
    Abbreviated titleLPAR-19
    CountrySouth Africa
    CityStellenbosch
    Period14/12/1319/12/13
    Internet address

    Keywords

    • Theorem Proving
    • Statistical Machine-Learning
    • Pattern Recognition
    • Lemma Discovery
    • Analogy

    Fingerprint Dive into the research topics of 'Proof-pattern recognition and lemma discovery in ACL2'. Together they form a unique fingerprint.

  • Projects

    Cite this

    Heras, J., Komendantskaya, E., Johansson, M., & Maclean, E. (2013). Proof-pattern recognition and lemma discovery in ACL2. In K. McMIllan, A. Middledorp, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings (pp. 389-406). (Lecture notes in computer science; Vol. 8312). Springer . https://doi.org/10.1007/978-3-642-45221-5_27