Proof-pattern recognition and lemma discovery in ACL2

  1. Heras, J. 2
  2. Komendantskaya, E. 2
  3. Johansson, M. 1
  4. Maclean, E. 3
  1. 1 Chalmers University of Technology
    info

    Chalmers University of Technology

    Gotemburgo, Suecia

    ROR https://ror.org/040wg7k59

  2. 2 University of Dundee
    info

    University of Dundee

    Dundee, Reino Unido

    ROR https://ror.org/03h2bxq36

  3. 3 University of Edinburgh
    info

    University of Edinburgh

    Edimburgo, Reino Unido

    ROR https://ror.org/01nrxwf90

Mostrar afiliaciones +
Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2013

Volumen: 8312 LNCS

Páginas: 389-406

Tipo: Artículo

DOI: 10.1007/978-3-642-45221-5_27 SCOPUS: 2-s2.0-84893944750 GOOGLE SCHOLAR

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

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. © Springer-Verlag 2013.