IsaCoSy: Synthesis of Inductive Theorems

Moa Johansson, Lucas Dixon, Alan Bundy

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

Abstract / Description of output

We have implemented a program for inductive theory formation, called IsaCoSy, which synthesises conjectures about recursively defined datatypes and functions. Only irreducible terms are generated, which keeps the search space tractably small. The synthesised terms are filtered through counter-example checking and then passed on to the automatic inductive prover IsaPlanner. Experiments have given promising results, with high recall of 83% for natural numbers and 100% for lists when compared to libraries for the Isabelle theorem prover. However, precision is somewhat lower, 38-63%.
Original languageEnglish
Title of host publicationWorkshop on Automated Mathematical Theory Exploration (Automatheo)
Number of pages4
Publication statusPublished - 2009
EventAUTOMATHEØ Workshop on Automated Mathematical Theory Exploration 2009 - Hagenberg, Austria
Duration: 29 Jun 200930 Jun 2009

Conference

ConferenceAUTOMATHEØ Workshop on Automated Mathematical Theory Exploration 2009
Country/TerritoryAustria
CityHagenberg
Period29/06/0930/06/09

Fingerprint

Dive into the research topics of 'IsaCoSy: Synthesis of Inductive Theorems'. Together they form a unique fingerprint.

Cite this