Machine Learning for Automated Inductive Theorem Proving

Yaqing Jiang; Petros Papapanagiotou; Jacques Fleuriot

doi:10.1007/978-3-319-99957-9_6

Machine Learning for Automated Inductive Theorem Proving

Yaqing Jiang, Petros Papapanagiotou, Jacques Fleuriot

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

Abstract / Description of output

Over the past few years, machine learning has been successfully combined with automated theorem provers to prove conjectures from proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in the proof assistant HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPS or the Boyer-Moore tool individually.

Original language	English
Title of host publication	Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018
Subtitle of host publication	Lecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018
Place of Publication	Suzhou, China
Publisher	Springer
Pages	87-103
Number of pages	16
ISBN (Electronic)	978-3-319-99957-9
ISBN (Print)	978-3-319-99956-2
DOIs	https://doi.org/10.1007/978-3-319-99957-9_6
Publication status	E-pub ahead of print - 22 Aug 2018
Event	13th International Conference on Artificial Intelligence and Symbolic Computation - Suzhou, China Duration: 16 Sept 2018 → 19 Sept 2018 http://aisc2018.cc4cm.org/index.html#cfp

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Volume	11110
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Name	Lecture Notes in Artificial Intelligence
Volume	11110

Conference

Conference	13th International Conference on Artificial Intelligence and Symbolic Computation
Abbreviated title	AISC 2018
Country/Territory	China
City	Suzhou
Period	16/09/18 → 19/09/18
Internet address	http://aisc2018.cc4cm.org/index.html#cfp

Access to Document

10.1007/978-3-319-99957-9_6

Machine Learning for Automated Inductive Theorem ProvingAccepted author manuscript, 282 KB

https://link.springer.com/chapter/10.1007/978-3-319-99957-9_6

ProofPeer: Collaborative Theorem Proving
Fleuriot, J. & Aspinall, D.
EPSRC
1/04/14 → 31/03/17
Project: Research

Cite this

Jiang, Y., Papapanagiotou, P., & Fleuriot, J. (2018). Machine Learning for Automated Inductive Theorem Proving. In Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018 : Lecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018 (pp. 87-103). (Lecture Notes in Computer Science; Vol. 11110), (Lecture Notes in Artificial Intelligence; Vol. 11110). Springer. Advance online publication. https://doi.org/10.1007/978-3-319-99957-9_6

Jiang, Yaqing ; Papapanagiotou, Petros ; Fleuriot, Jacques. / Machine Learning for Automated Inductive Theorem Proving. Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018 : Lecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018. Suzhou, China : Springer, 2018. pp. 87-103 (Lecture Notes in Computer Science). (Lecture Notes in Artificial Intelligence).

@inproceedings{c8d4d86ee71c4e44b121a314097c4803,

title = "Machine Learning for Automated Inductive Theorem Proving",

abstract = "Over the past few years, machine learning has been successfully combined with automated theorem provers to prove conjectures from proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in the proof assistant HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPS or the Boyer-Moore tool individually.",

author = "Yaqing Jiang and Petros Papapanagiotou and Jacques Fleuriot",

year = "2018",

month = aug,

day = "22",

doi = "10.1007/978-3-319-99957-9_6",

language = "English",

isbn = "978-3-319-99956-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "87--103",

booktitle = "Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018",

note = "13th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2018 ; Conference date: 16-09-2018 Through 19-09-2018",

url = "http://aisc2018.cc4cm.org/index.html#cfp",

}

Jiang, Y, Papapanagiotou, P & Fleuriot, J 2018, Machine Learning for Automated Inductive Theorem Proving. in Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018 : Lecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018. Lecture Notes in Computer Science, vol. 11110, Lecture Notes in Artificial Intelligence, vol. 11110, Springer, Suzhou, China, pp. 87-103, 13th International Conference on Artificial Intelligence and Symbolic Computation, Suzhou, China, 16/09/18. https://doi.org/10.1007/978-3-319-99957-9_6

Machine Learning for Automated Inductive Theorem Proving. / Jiang, Yaqing; Papapanagiotou, Petros; Fleuriot, Jacques.
Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018 : Lecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018. Suzhou, China: Springer, 2018. p. 87-103 (Lecture Notes in Computer Science; Vol. 11110), (Lecture Notes in Artificial Intelligence; Vol. 11110).

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

TY - GEN

T1 - Machine Learning for Automated Inductive Theorem Proving

AU - Jiang, Yaqing

AU - Papapanagiotou, Petros

AU - Fleuriot, Jacques

PY - 2018/8/22

Y1 - 2018/8/22

N2 - Over the past few years, machine learning has been successfully combined with automated theorem provers to prove conjectures from proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in the proof assistant HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPS or the Boyer-Moore tool individually.

AB - Over the past few years, machine learning has been successfully combined with automated theorem provers to prove conjectures from proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in the proof assistant HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPS or the Boyer-Moore tool individually.

U2 - 10.1007/978-3-319-99957-9_6

DO - 10.1007/978-3-319-99957-9_6

M3 - Conference contribution

SN - 978-3-319-99956-2

T3 - Lecture Notes in Computer Science

SP - 87

EP - 103

BT - Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018

PB - Springer

CY - Suzhou, China

T2 - 13th International Conference on Artificial Intelligence and Symbolic Computation

Y2 - 16 September 2018 through 19 September 2018

ER -

Jiang Y, Papapanagiotou P, Fleuriot J. Machine Learning for Automated Inductive Theorem Proving. In Proceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018 : Lecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018. Suzhou, China: Springer. 2018. p. 87-103. (Lecture Notes in Computer Science). (Lecture Notes in Artificial Intelligence). Epub 2018 Aug 22. doi: 10.1007/978-3-319-99957-9_6

Machine Learning for Automated Inductive Theorem Proving

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Projects

ProofPeer: Collaborative Theorem Proving

Cite this