Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/s10817-010-9193-y | J. Autom. Reasoning |
Keywords | Field | DocType |
Theory formation,Induction,Synthesis,Theorem proving,Lemma discovery | Discrete mathematics,Free variables and bound variables,Computer science,IsaPlanner,Automated theorem proving,Algorithm,Conjecture,Gas meter prover,Proof assistant | Journal |
Volume | Issue | ISSN |
47 | 3 | 0168-7433 |
Citations | PageRank | References |
40 | 1.70 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Moa Johansson | 1 | 121 | 10.74 |
| Lucas Dixon | 2 | 1823 | 90.35 |
| A. Bundy | 3 | 3713 | 532.03 |