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