|
Published Articles >> Table of Contents >> Abstract
Eighth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06)
pp. 17-22
MATHsAiD: A Mathematical Theorem Discovery Tool
Roy L. McCasland
Alan Bundy, University of Edinburgh, UK
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SYNASC.2006.51
Send link to a friend
| Abstract |
|
In the field of automated reasoning, one of the most challenging
(even if, perhaps, somewhat overlooked) problems
thus far has been to develop a means of discerning, from
amongst all the truths that can be discovered and proved,
those which are either useful or interesting enough to be
worth recording. As for human reasoning, mathematicians
are well known for their predilection towards designating
certain discoveries as theorems, lemmas, corollaries, etc.,
whilst relegating all others as relatively unimportant. However,
precisely how mathematicians determine which results
to keep, and which to discard, is perhaps not so well
known. Nevertheless, this practice is an essential part of the
mathematical process, as it allows mathematicians to manage
what would otherwise be an overwhelming amount of
knowledge.
MATHsAiD is a system intended for use by research
mathematicians, and is designed to produce high quality
theorems, as recognised by mathematicians, within a given
theory. The only input required is a set of axioms and definitions
for each theory. In this paper we briefly describe
some of the more important methods used by MATHsAiD,
most of which are based primarily on the human mathematical
process.
|
 Additional Information
|
Citation:
Roy L. McCasland, Alan Bundy,
"MATHsAiD: A Mathematical Theorem Discovery Tool,"
synasc,
pp. 17-22,
Eighth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06),
2006
|
|
