Proof-Pattern Recognition and Lemma Discovery in ACL2

J. Heras; E. Komendantskaya; M. Johansson; E. Maclean

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

Proof-Pattern Recognition and Lemma Discovery in ACL2

J. Heras, E. Komendantskaya, M. Johansson, E. Maclean

School of Informatics

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

Abstract / Description of output

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
Publisher	Springer
Pages	389-406
Number of pages	18
ISBN (Electronic)	978-3-642-45221-5
ISBN (Print)	978-3-642-45220-8
DOIs	https://doi.org/10.1007/978-3-642-45221-5_27
Publication status	Published - 1 Aug 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	8312
ISSN (Print)	0302-9743

Keywords / Materials (for Non-textual outputs)

Computer Science - Logic in Computer Science

Access to Document

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

http://link.springer.com/chapter/10.1007%2F978-3-642-45221-5_27

A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A., Bundy, A., Grov, G., Ireland, A. & Jones, C. B.
EPSRC
1/04/10 → 31/03/14
Project: Research

Cite this

Heras, J., Komendantskaya, E., Johansson, M., & Maclean, E. (2013). Proof-Pattern Recognition and Lemma Discovery in ACL2. In 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

@inproceedings{d04d3bec0ced44c5b66e3cb863f8c051,

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 = "Computer Science - Logic in Computer Science",

author = "J. Heras and E. Komendantskaya and M. Johansson and E. Maclean",

year = "2013",

month = aug,

day = "1",

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

language = "English",

isbn = "978-3-642-45220-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "389--406",

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

address = "United Kingdom",

}

Heras, J, Komendantskaya, E, Johansson, M & Maclean, E 2013, Proof-Pattern Recognition and Lemma Discovery in ACL2. in 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, pp. 389-406. https://doi.org/10.1007/978-3-642-45221-5_27

Proof-Pattern Recognition and Lemma Discovery in ACL2. / Heras, J.; Komendantskaya, E.; Johansson, M. et al.
Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. 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, J.

AU - Komendantskaya, E.

AU - Johansson, M.

AU - Maclean, E.

PY - 2013/8/1

Y1 - 2013/8/1

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 - Computer Science - Logic in Computer Science

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

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

M3 - Conference contribution

SN - 978-3-642-45220-8

T3 - Lecture Notes in Computer Science

SP - 389

EP - 406

BT - Logic for Programming, Artificial Intelligence, and Reasoning

PB - Springer

ER -

Heras J, Komendantskaya E, Johansson M, Maclean E. Proof-Pattern Recognition and Lemma Discovery in ACL2. In Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. 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 / Description of output

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

A14FM : using A1 to aid automation of proof search in formal methods

Cite this