Edinburgh Research Explorer

Typed meta-interpretive learning for proof strategies

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

  • Colin Farquhar
  • Gudmund Grov
  • Andrew Cropper
  • Stephen Muggleton
  • Alan Bundy

Related Edinburgh Organisations

Access status

Open

Documents

  • Download as Adobe PDF

    Final published version, 651 KB, PDF-document

    License: Creative Commons: Attribution (CC-BY)

http://ceur-ws.org/Vol-1636/
Original languageEnglish
Title of host publicationLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015)
PublisherCEUR Workshop Proceedings (CEUR-WS.org)
Pages1-16
Number of pages16
StatePublished - 13 Jul 2016

Abstract

Formal verification of computer programs is increasingly used in industry. A popular technique is interactive theorem proving, used for instance by Intel in HOL light. The ability to learn and re-apply proof strategies from a small set of proofs would significantly increase the productivity of these systems, and make them more cost-effective to use. Previous learning attempts have had limited success, which we believe is a result of missing key goal properties in the strategies. Capturing such properties requires predicate invention, and the only state-of-the-art ILP technique which supports this is meta-interpretive learning (MIL). We show that MIL is applicable to this problem, but that without type information it offers limited improvements in quality over previous work. We then extend MIL with types and give preliminary results indicating that this extension learns better-quality strategies with suitable goal properties. We also show that the quality of the learned strategies can be further enhanced through the use of dependent learning.

Download statistics

No data available

ID: 26604203