Automated Discovery of Inductive Theorems

Roy McCasland, Alan Bundy, Autexier Serge

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Inductive mathematical theorems have, as a rule, historically been quite difficult to prove – both for mathematics students and for auto- mated theorem provers. That said, there has been considerable progress over the past several years, within the automated reasoning community, towards proving some of these theorems. However, little work has been done thus far towards automatically discovering them. In this paper we present our methods of discovering (as well as proving) inductive theorems, within an automated system. These methods have been tested over the natural num- bers, with regards to addition and multiplication, as well as to exponents of group elements.
Original languageEnglish
JournalStudies in Logic, Grammar and Rhetoric
Issue number23
Publication statusPublished - 2007


Dive into the research topics of 'Automated Discovery of Inductive Theorems'. Together they form a unique fingerprint.

Cite this