IsaCoSy: Synthesis of Inductive Theorems

Moa Johansson; Lucas Dixon; Alan Bundy

IsaCoSy: Synthesis of Inductive Theorems

Moa Johansson, Lucas Dixon, Alan Bundy

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Workshop on Automated Mathematical Theory Exploration (Automatheo)
Number of pages	4
Publication status	Published - 2009
Event	AUTOMATHEØ Workshop on Automated Mathematical Theory Exploration 2009 - Hagenberg, Austria Duration: 29 Jun 2009 → 30 Jun 2009

Conference

Conference	AUTOMATHEØ Workshop on Automated Mathematical Theory Exploration 2009
Country/Territory	Austria
City	Hagenberg
Period	29/06/09 → 30/06/09

Access to Document

Full textAccepted author manuscript, 109 KB

Cite this

@inproceedings{d40cf3d5cbd64349bcfddfc48ac401d7,

title = "IsaCoSy: Synthesis of Inductive Theorems",

abstract = "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%.",

author = "Moa Johansson and Lucas Dixon and Alan Bundy",

year = "2009",

language = "English",

booktitle = "Workshop on Automated Mathematical Theory Exploration (Automatheo)",

note = "AUTOMATHE{\O} Workshop on Automated Mathematical Theory Exploration 2009 ; Conference date: 29-06-2009 Through 30-06-2009",

}

TY - GEN

T1 - IsaCoSy: Synthesis of Inductive Theorems

AU - Johansson, Moa

AU - Dixon, Lucas

AU - Bundy, Alan

PY - 2009

Y1 - 2009

N2 - 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%.

AB - 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%.

M3 - Conference contribution

BT - Workshop on Automated Mathematical Theory Exploration (Automatheo)

T2 - AUTOMATHEØ Workshop on Automated Mathematical Theory Exploration 2009

Y2 - 29 June 2009 through 30 June 2009

ER -

IsaCoSy: Synthesis of Inductive Theorems

Abstract

Conference

Access to Document

Fingerprint

Cite this