This page contains links to the results produced by MATHsAiD, in
several theories. For each theory, one can find the Axioms
provided to MATHsAiD, the Theorems discovered and proven by MATHsAiD,
and the (automatically generated) sequence of hypotheses which was used
in the discovery process.
Each member of the hypotheses sequence consists of three parts --
separated by (square) brackets. Inside the first set of brackets,
are the hypotheses themselves. The next set of brackets contain
the "terms of interest" (if any are provided), and similarly, the last
set of brackets contain the "axioms of interest". The number at
the end of each line indicates the cumulative number of Theorems
discovered in the given theory, subsequent to those hypotheses (on that
line) being investigated. Hence, one can compare each set of
hypotheses to the Theorems, and determine which Theorems correspond to
which hypotheses/terms or axioms of interest. NOTE: occasionally, the
second pair of brackets contains a "prove" or an "induct". In the
former case, MATHsAiD tries to prove the corresponding conjecture,
which is the convers either of one of the given axioms, or of a
previously discovered Theorem. In the latter case, MATHsAiD will
try to discover some inductive Theorem about the given term of interest.
The three different versions of "natural number" each focus on a
different aspect of the theory. For instance, the Positive
Integers theory looks at "less than", while Nstar focuses on induction.
Similarly, the Natural Numbers theory also focuses on induction, but
uses a different representation from either of the other theories, and
also includes the number 0.
Last Updated on 23/06/2006
By Roy McCasland