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 -