CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Proof-pattern recognition and lemma discovery in ACL2

J. Heras ; E. Komendantskaya ; Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; E. Maclean
Lecture Notes in Computer Science (0302-9743). Vol. 8312 (2013), p. 389-406.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Analogy , Lemma discovery , Pattern recognition , Statistical machine-learning , Theorem proving



Denna post skapades 2015-05-05. Senast ändrad 2016-04-29.
CPL Pubid: 216414

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)