Projects per year
Abstract / Description of output
We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on ?schemes?, which are formulae in higherorder logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of a theory can be used, not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theoryformation systems. We exploit associativecommutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth?Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.
Original language  English 

Pages (fromto)  16371646 
Number of pages  10 
Journal  Expert Systems with Applications 
Volume  39 
Issue number  2 
DOIs  
Publication status  Published  2012 
Fingerprint
Dive into the research topics of 'Schemebased theorem discovery and concept invention'. Together they form a unique fingerprint.Projects
 2 Finished


Integration and Interaction of multiple mathematical reasoning processes
Bundy, A., Colton, S., Aspinall, D., Dennis, L., Fleuriot, J., Georgieva, L., Ireland, A., Jackson, P. & Smaill, A.
1/04/07 → 31/03/11
Project: Research