Conjecture Synthesis for Inductive Theories

Moa Johansson, Lucas Dixon, Alan Bundy

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
Pages (from-to)251-289
Number of pages39
JournalJournal of Automated Reasoning
Volume47
Issue number3
DOIs
Publication statusPublished - Oct 2011

Keywords

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

Cite this