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

Open Access permissions



  • Download as Adobe PDF

    Final published version, 651 KB, PDF document

    Licence: Creative Commons: Attribution (CC-BY)

Original languageEnglish
Title of host publicationLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015)
PublisherCEUR Workshop Proceedings (CEUR-WS.org)
Number of pages16
Publication statusPublished - 13 Jul 2016
EventLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015) - Kyoto, Japan
Duration: 20 Aug 201522 Aug 2015


ConferenceLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015)
Abbreviated titleLBP-ILP 2015
Internet address


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.


Late-breaking papers proceedings of ILP 2015 (LBP-ILP 2015)


Kyoto, Japan

Event: Conference

Download statistics

No data available

ID: 26604203