The EPGY Theorem Proving Environment
Overview
The EPGY TheoremProving Environment is a tool that allows students to
compose logically valid mathematical proofs on the computer. Currently, the
system is being used by students in Euclidean geometry (M015).
Beginning with given statements and a proof goal, students may
construct a formal proof by applying builtin proof strategies and
logical inference rules, either forwards from the given statements or
backwards from the goal. Students can also apply a wide selection of
mathematical rules for manipulating equations, inequalities, and
individual terms. Additionally, a student can enter a statement he or
she believes is valid, and useful for the proof, and attempt to verify
it using other proof lines together with axioms, definitions and
theorems from a database of facts pertinent to the course.
The interface and format are meant to allow students to compose their
proofs naturally, where their final proofs are representative of those
found in standard mathematical practice.
Page maintained by: David McMath ( mcdave@epgy.stanford.edu)
Last modified: Thu Nov 29 13:01:32 PST 2001
© 2001, EPGY Stanford University. All rights reserved.
