A Combinator Language for Theorem Discovery

Phil Scott, Jacques Fleuriot

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

Abstract / Description of output

We define and implement a combinator language for intermediate lemma discovery. We start by generalising an algebraic data-structure for unbounded search and then extend it to support case-analysis. With our language defined, we expect users to be able to write discoverers which collaborate intelligently in specific problem domains. For now, the language integrates rewriting, forward-deduction, and case-analysis and discovers lemmas concurrently based on an interactive proof context. We argue that the language is most suitable for adding domain-specific automation to mechanically formalised proofs written in a forward-style, and we show how the language is used via a case-study in geometry.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings
EditorsJohan Jeuring, John Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge
PublisherSpringer-Verlag GmbH
Pages371-385
Number of pages15
ISBN (Electronic)978-3-642-31374-5
ISBN (Print)978-3-642-31373-8
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume7362
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'A Combinator Language for Theorem Discovery'. Together they form a unique fingerprint.

Cite this