Edinburgh Research Explorer

Machine Learning for Automated Inductive Theorem Proving

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://link.springer.com/chapter/10.1007/978-3-319-99957-9_6
Original languageEnglish
Title of host publicationProceedings of the 13th International Artificial Intelligence and Symbolic Computation (AISC) Conference 2018
Subtitle of host publicationLecture Notes in Artificial Intelligence, Volume 11110, pages 87-103, 2018
Place of PublicationSuzhou, China
PublisherSpringer, Cham
Pages87-103
Number of pages16
ISBN (Electronic)978-3-319-99957-9
ISBN (Print)978-3-319-99956-2
DOIs
Publication statusE-pub ahead of print - 22 Aug 2018
Event13th International Conference on Artificial Intelligence and Symbolic Computation - Suzhou, China
Duration: 16 Sep 201819 Sep 2018
http://aisc2018.cc4cm.org/index.html#cfp

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume11110
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameLecture Notes in Artificial Intelligence
Volume11110

Conference

Conference13th International Conference on Artificial Intelligence and Symbolic Computation
Abbreviated titleAISC 2018
CountryChina
CitySuzhou
Period16/09/1819/09/18
Internet address

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.

Event

Download statistics

No data available

ID: 74941929