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, Cham
CY - Suzhou, China
T2 - 13th International Conference on Artificial Intelligence and Symbolic Computation
Y2 - 16 September 2018 through 19 September 2018
ER -