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: http://hdl.handle.net/1842/4745

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

Files in This Item:

File Description SizeFormat
BundyA_Formalising Term.pdf244.7 kBAdobe PDFView/Open
Title: Formalising Term Synthesis for Isacosy
Authors: Johansson, Moa
Dixon, Lucas
Bundy, Alan
Issue Date: 2010
Journal Title: Workshop on Automated Mathematical Theory Exploration (Automatheo)
Abstract: IsaCoSy is a theory formation system for inductive theories. It synthesises conjectures and uses the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a formal account of the algorithms implemented in the system, and prove their correctness. In particular, we show that IsaCoSy only produces irreducible terms, using constraints generated from the left-hand sides of a set of rewrite rules.
URI: http://dream.inf.ed.ac.uk/events/automatheo-2010/
http://hdl.handle.net/1842/4745
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