Proof-pattern recognition and lemma discovery in ACL2

Jonathan Heras; Ekaterina Komendantskaya; Moa Johansson; Ewen Maclean

doi:10.1007/978-3-642-45221-5_27

Proof-pattern recognition and lemma discovery in ACL2

Jonathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

25 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 language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication	19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings
Editors	Ken McMIllan, Aart Middledorp, Andrei Voronkov
Place of Publication	Berlin
Publisher	Springer
Pages	389-406
Number of pages	18
ISBN (Electronic)	9783642452215
ISBN (Print)	9783642452208
DOIs	https://doi.org/10.1007/978-3-642-45221-5_27
Publication status	Published - 2013
Event	19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Stellenbosch, South Africa Duration: 14 Dec 2013 → 19 Dec 2013 http://www.cs.sun.ac.za/lpar-19/

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	8312

Conference

Conference	19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Abbreviated title	LPAR-19
Country/Territory	South Africa
City	Stellenbosch
Period	14/12/13 → 19/12/13
Internet address	http://www.cs.sun.ac.za/lpar-19/

Keywords

Theorem Proving
Statistical Machine-Learning
Pattern Recognition
Lemma Discovery
Analogy

Access to Document

10.1007/978-3-642-45221-5_27

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)
Komendantskaya, E. (Investigator)
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research

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

Heras, Jonathan ; Komendantskaya, Ekaterina ; Johansson, Moa et al. / Proof-pattern recognition and lemma discovery in ACL2. Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. editor / Ken McMIllan ; Aart Middledorp ; Andrei Voronkov. Berlin : Springer , 2013. pp. 389-406 (Lecture notes in computer science).

@inproceedings{8bbf8a8b6b4642c8b6fbe4b893f01ed5,

title = "Proof-pattern recognition and lemma discovery in ACL2",

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.",

keywords = "Theorem Proving, Statistical Machine-Learning, Pattern Recognition, Lemma Discovery, Analogy",

author = "Jonathan Heras and Ekaterina Komendantskaya and Moa Johansson and Ewen Maclean",

year = "2013",

doi = "10.1007/978-3-642-45221-5_27",

language = "English",

isbn = "9783642452208",

series = "Lecture notes in computer science",

publisher = "Springer ",

pages = "389--406",

editor = "Ken McMIllan and Aart Middledorp and Andrei Voronkov",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",

note = "19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-19 ; Conference date: 14-12-2013 Through 19-12-2013",

url = "http://www.cs.sun.ac.za/lpar-19/",

}

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. Lecture notes in computer science, vol. 8312, Springer , Berlin, pp. 389-406, 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa, 14/12/13. https://doi.org/10.1007/978-3-642-45221-5_27

Proof-pattern recognition and lemma discovery in ACL2. / Heras, Jonathan; Komendantskaya, Ekaterina; Johansson, Moa et al.
Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. ed. / Ken McMIllan; Aart Middledorp; Andrei Voronkov. Berlin: Springer , 2013. p. 389-406 (Lecture notes in computer science; Vol. 8312).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Proof-pattern recognition and lemma discovery in ACL2

AU - Heras, Jonathan

AU - Komendantskaya, Ekaterina

AU - Johansson, Moa

AU - Maclean, Ewen

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

KW - Theorem Proving

KW - Statistical Machine-Learning

KW - Pattern Recognition

KW - Lemma Discovery

KW - Analogy

U2 - 10.1007/978-3-642-45221-5_27

DO - 10.1007/978-3-642-45221-5_27

M3 - Conference contribution

SN - 9783642452208

T3 - Lecture notes in computer science

SP - 389

EP - 406

BT - Logic for Programming, Artificial Intelligence, and Reasoning

A2 - McMIllan, Ken

A2 - Middledorp, Aart

A2 - Voronkov, Andrei

PB - Springer

CY - Berlin

T2 - 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning

Y2 - 14 December 2013 through 19 December 2013

ER -

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

Proof-pattern recognition and lemma discovery in ACL2

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this