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 courses in Euclidean geometry (M015) and linear algebra (M51A), and it is scheduled for use in courses in multivariable calculus and differential equations. Eventually, this system will be available in all of EPGY's proof-intensive mathematics courses.

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.