Proof-pattern recognition and lemma discovery in ACL2
- Heras, J. 2
- Komendantskaya, E. 2
- Johansson, M. 1
- Maclean, E. 3
-
1
Chalmers University of Technology
info
-
2
University of Dundee
info
-
3
University of Edinburgh
info
ISSN: 0302-9743
Argitalpen urtea: 2013
Alea: 8312 LNCS
Orrialdeak: 389-406
Mota: Artikulua
Beste argitalpen batzuk: Lecture Notes in Computer Science
Laburpena
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.