Conjecture Synthesis for Inductive Theories
Conjecture Synthesis for Inductive Theories
复制标题
归纳理论的猜想综合
DOI：
10.1007/s10817-010-9193-y
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
A. Bundy
中科院分区：
文献类型：
--
作者：
Moa Johansson;L. Dixon;A. Bundy
我们已经开发了一个用于归纳理论形成的程序，称为Isacosy，该程序从可用常数和自由变量中构成了“自下而上”的猜想。并传递给自动归纳诗意工具。对综合过程的其他约束。 isabelle库。
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.
影响因子：
--
作者：
Alan Bundy (Author)
通讯作者：
Alan Bundy (Author)