Edinburgh Research Explorer

Automated Discovery of Inductive Theorems

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions



Original languageEnglish
JournalStudies in Logic, Grammar and Rhetoric
Issue number23
Publication statusPublished - 2007


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.

Download statistics

No data available

ID: 402045