DocumentCode :
3427540
Title :
MATHsAiD: A Mathematical Theorem Discovery Tool
Author :
McCasland, Roy L. ; Bundy, Alan
Author_Institution :
Sch. of Informatics, Edinburgh Univ., Scotland
fYear :
2006
fDate :
Sept. 2006
Firstpage :
17
Lastpage :
22
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
Keywords :
mathematics computing; theorem proving; MATHsAiD; automated reasoning; high quality theorems; human mathematical process; human reasoning; mathematical theorem discovery tool; mathematicians; Disk recording; Filtering; Filters; Graphical user interfaces; Humans; Informatics; Java; Knowledge management; Mathematics; Mercury (metals);
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Symbolic and Numeric Algorithms for Scientific Computing, 2006. SYNASC '06. Eighth International Symposium on
Conference_Location :
Timisoara
Print_ISBN :
0-7695-2740-X
Type :
conf
DOI :
10.1109/SYNASC.2006.51
Filename :
4090292
Link To Document :
بازگشت