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 , and have used it in a non-trivial setting, namely incidence-reasoning for geometry theorem proving.
|Title of host publication||Interactive Theorem Proving|
|Subtitle of host publication||Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings|
|Editors||Marko van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk|
|Number of pages||6|
|Publication status||Published - 2011|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|