@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",
}