Show simple item record

Journal of Automated Reasoning

dc.contributor.authorJohansson, Moa
dc.contributor.authorDixon, Lucas
dc.contributor.authorBundy, Alan
dc.date.accessioned2011-02-01T13:29:37Z
dc.date.available2011-02-01T13:29:37Z
dc.date.issued2010
dc.identifier.issn0168-7433en
dc.identifier.urihttp://www.springerlink.com/content/bk711q2u247mr967/en
dc.identifier.urihttp://hdl.handle.net/1842/4746
dc.description.abstractWe 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.en
dc.language.isoenen
dc.publisherSpringerLinken
dc.subjectTheory formationen
dc.subjectInductionen
dc.subjectSynthesisen
dc.subjectTheorem provingen
dc.subjectLemma discoveryen
dc.titleConjecture Synthesis for Inductive Theoriesen
dc.typeArticleen
dc.identifier.doi10.1007/s10817-010-9193-yen
rps.titleJournal of Automated Reasoningen
dc.date.updated2011-02-01T13:29:37Z
dc.identifier.eIssn1573-0670en


Files in this item

This item appears in the following Collection(s)

Show simple item record