Composable Discovery Engines for Interactive Theorem Proving

Phil Scott, Jacques Fleuriot

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

Abstract

We describe a framework to integrate discovery engines with interactive theorem proving, and define an algebra for composing them. Discovery engines can be tailored to specific domains and invoked concurrently as the user writes the proof. The engines collaborate with the user by inferring facts from the current goal context, and providing new theorems to advance the proof. We have developed the system in HOL Light [1], and have used it in a non-trivial setting, namely incidence-reasoning for geometry theorem proving.
Original languageEnglish
Title of host publicationInteractive Theorem Proving
Subtitle of host publicationSecond International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings
EditorsMarko van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk
PublisherSpringer-Verlag GmbH
Pages370-375
Number of pages6
ISBN (Print)978-3-642-22862-9
DOIs
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume6898

Fingerprint Dive into the research topics of 'Composable Discovery Engines for Interactive Theorem Proving'. Together they form a unique fingerprint.

Cite this