@inproceedings{c608364a57c943bc9b18d893688067d6,

title = "Composable Discovery Engines for Interactive Theorem Proving",

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.",

author = "Phil Scott and Jacques Fleuriot",

year = "2011",

doi = "10.1007/978-3-642-22863-6_28",

language = "English",

isbn = "978-3-642-22862-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag GmbH",

pages = "370--375",

editor = "{van Eekelen}, Marko and Herman Geuvers and Julien Schmaltz and Freek Wiedijk",

booktitle = "Interactive Theorem Proving",

}