A Combinator Language for Theorem Discovery

摘要

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.