Fleuriot, Jacques

Jackson, Paul

Jiang, Yaqing

other

2019-10-23T13:30:06Z

2019-10-23T13:30:06Z

2019-11-23

Over the past few years, machine learning has been successfully combined with automated theorem provers (ATPs) to prove conjectures from various 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 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. An attempt to add the support for non-recursive type to the Boyer-Moore waterfall model is made by looking at proof automation for finite sets. We also test the framework in a program verification setting by looking at proofs about sorting algorithms in Hoare Logic.

https://hdl.handle.net/1842/36234

en

The University of Edinburgh

Jiang Y., Papapanagiotou P., Fleuriot J. (2018) Machine Learning for Inductive Theorem Proving. In: Fleuriot J.,Wang D., Calmet J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2018. Lecture Notes in Computer Science, vol 11110. Springer, Cham

mathematical proofs

automated theorem provers

machine learning

Boyer-Moore model

Machine learning for inductive theorem proving

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy