TY - JOUR
T1 - Ascertaining Mathematical Theorems
AU - McCasland, R.
AU - Bundy, Alan
AU - Smith, P.
PY - 2006
Y1 - 2006
N2 - Whereas to most logicians, the word "theorem" refers to any statement which has been shown to be true, to mathematicians, the workd "Theorem" is, relatively speaking, rarely applied, and denotes something fra more special. In this paper, we examine some of the underlying reasons behind this difference in terminology, and we show how this discrepancy might be exploited, in order to build a computer system which automatically selects the latter type of "Theorems" from amongst the former. Indeed, we have begun building the automated discovery system MATHsAiD, the design of which is based upon our research. We provide some preliminary results produced by this system, and compare these results to Theorems appearing in various mathematics textbooks.
AB - Whereas to most logicians, the word "theorem" refers to any statement which has been shown to be true, to mathematicians, the workd "Theorem" is, relatively speaking, rarely applied, and denotes something fra more special. In this paper, we examine some of the underlying reasons behind this difference in terminology, and we show how this discrepancy might be exploited, in order to build a computer system which automatically selects the latter type of "Theorems" from amongst the former. Indeed, we have begun building the automated discovery system MATHsAiD, the design of which is based upon our research. We provide some preliminary results produced by this system, and compare these results to Theorems appearing in various mathematics textbooks.
KW - automated theorem generation
KW - Mathematical Reasoning
U2 - 10.1016/j.entcs.2005.11.021
DO - 10.1016/j.entcs.2005.11.021
M3 - Article
VL - 151
SP - 21
EP - 38
JO - Electronic Notes in Theoretical Computer Science
T2 - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
IS - 1
ER -