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