Mathdialog is a tool to develop and navigate interactively through definitions,
theorems, and proofs at the undergraduate level. It has agile ways to provide
answers to frequently asked questions in mathematical proofs, such as: "What
is its definition?", "Where does the justification for that hypothesis come
from?", "What is the justification for this step?", "What does the theorem
that justifies that hypothesis say?", and "Where does this hypothesis come from?"
The Mathdialog NUCLEUS is the minimal set of about one hundred definitions and
theorems needed for the system to work. You can consult them all by clicking
"Start Mathdialog." To begin, we recommend the following, but feel free to
consult any others:
Theorems:
BIN_UNION_P01, BIN_UNION_P05, NOEMP_P01, EMPTY_P01, GROUP_P01, GROUP_P04,
INV_GROUP_UNIQUENESS, KURATOWSKI_PAIR, and CART_PROD_EXIST.
Definitions:
FUNC, FUNC_IN, FUNC_TO, FUNC_IN_TO, INDUCTIVE, INFIMUM, MAXIMAL, LOW_BOUND.