- Abstract:
-
Inductive mathematical theorems have, as a rule, historically been quite difficult to prove - both for mathematics students and for automated 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 numbers, with regards to addition and multiplication, as well as to exponents of group elements.
- Copyright:
- 2007 by The University of Bialystok. All Rights Reserved
- Links To Paper
- 1st Link
- Bibtex format
- @InBook{EDI-INF-RR-1097,
- author = {
Roy McCasland
and Alan Bundy
and Serge Autexier
},
- title = {Automated discovery of inductive theorems.},
- book title = {From Insight to Proof},
- publisher = {University of Bialystok},
- year = 2007,
- month = {Jul},
- volume = {10(23)},
- pages = {135-150},
- url = {http://mizar.org/trybulec65/},
- }
|
