The EPGY Theorem Proving Environment

Overview

The EPGY Theorem-Proving 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 built-in 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.