Formalising Term Synthesis for Isacosy

Moa Johansson; Lucas Dixon; Alan Bundy

Formalising Term Synthesis for Isacosy

Moa Johansson, Lucas Dixon, Alan Bundy

School of Informatics

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

Abstract / Description of output

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.

Original language	English
Title of host publication	Workshop on Automated Mathematical Theory Exploration (Automatheo)
Publisher	Automatheo - IJCAR 2010
Publication status	Published - 2010

Access to Document

Full textAccepted author manuscript, 245 KB

Cite this

@inproceedings{2fdf828d62a748f0bd3e403e20735174,

title = "Formalising Term Synthesis for Isacosy",

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

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

year = "2010",

language = "English",

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

publisher = "Automatheo - IJCAR 2010 ",

}

TY - GEN

T1 - Formalising Term Synthesis for Isacosy

AU - Johansson, Moa

AU - Dixon, Lucas

AU - Bundy, Alan

PY - 2010

Y1 - 2010

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

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

M3 - Conference contribution

BT - Workshop on Automated Mathematical Theory Exploration (Automatheo)

PB - Automatheo - IJCAR 2010

ER -

Formalising Term Synthesis for Isacosy

Abstract / Description of output

Access to Document

Fingerprint

Cite this