TY - JOUR
T1 - Conjecture Synthesis for Inductive Theories
AU - Johansson,Moa
AU - Dixon,Lucas
AU - Bundy,Alan
PY - 2011/10
Y1 - 2011/10
N2 - We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures 'bottom-up' from the available constants and free variables. The synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover IsaPlanner. The main technical contribution is the presentation of a constraint mechanism for synthesis. As theorems are discovered, this generates additional constraints on the synthesis process. We evaluate IsaCoSy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the Isabelle system. The results show that IsaCoSy produces most, and sometimes all, of the theorems in the Isabelle libraries. The number of additional un-interesting theorems are small enough to be easily pruned by hand.
AB - We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures 'bottom-up' from the available constants and free variables. The synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover IsaPlanner. The main technical contribution is the presentation of a constraint mechanism for synthesis. As theorems are discovered, this generates additional constraints on the synthesis process. We evaluate IsaCoSy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the Isabelle system. The results show that IsaCoSy produces most, and sometimes all, of the theorems in the Isabelle libraries. The number of additional un-interesting theorems are small enough to be easily pruned by hand.
KW - Theory formation
KW - Induction
KW - Synthesis
KW - Theorem proving
KW - Lemma discovery
UR - http://www.scopus.com/inward/record.url?scp=80053051684&partnerID=8YFLogxK
U2 - 10.1007/s10817-010-9193-y
DO - 10.1007/s10817-010-9193-y
M3 - Article
VL - 47
SP - 251
EP - 289
JO - Journal of Automated Reasoning
T2 - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
SN - 0168-7433
IS - 3
ER -