Edinburgh Research Explorer

Conjecture Synthesis for Inductive Theories

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Access status

Open

Documents

http://link.springer.com/article/10.1007%2Fs10817-010-9193-y
Original languageEnglish
Pages (from-to)251-289
Number of pages39
JournalJournal of Automated Reasoning
Volume47
Issue number3
DOIs
StatePublished - Oct 2011

Abstract

We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures 'bottom-up' from the available constants and free variables. The synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover IsaPlanner. The main technical contribution is the presentation of a constraint mechanism for synthesis. As theorems are discovered, this generates additional constraints on the synthesis process. We evaluate IsaCoSy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the Isabelle system. The results show that IsaCoSy produces most, and sometimes all, of the theorems in the Isabelle libraries. The number of additional un-interesting theorems are small enough to be easily pruned by hand.

Research areas

  • Theory formation, Induction, Synthesis, Theorem proving, Lemma discovery

Download statistics

No data available

ID: 48457