Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >

Please use this identifier to cite or link to this item:

This item has been viewed 2 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
BundyA_IsaCoSy Synthesis.pdf109.28 kBAdobe PDFView/Open
Title: Isacosy: Synthesis of Inductive Theorems
Authors: Dixon, Lucas
Bundy, Alan
Johansson, Moa
Issue Date: 2009
Journal Title: Workshop on Automated Mathematical Theory Exploration (Automatheo)
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%.
Appears in Collections:Informatics Publications

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy