MATHsAiD Results

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.

Theory Axioms
Theorems Hypotheses
Sets set axms
set thms
set hyps
Positive Integers Zplus axms
Zplus thms
Zplus hyps
Nstar Nstar axms
Nstar thms Nstar hyps
Natural Numbers nat axms
nat thms
nat hyps
Groups group axms
group thms
group hyps

Last Updated on 23/06/2006
By Roy McCasland