The EPGY Theorem Proving Environment

Downloads

Binaries

The Theorem Proving Environment is designed to run within the EPGY Course System. We have made a stand-alone version available, however, for people who would like to experiment with the program. In particular, all "Undo/Redo" information is stored within a proof file, so the user may retrace the steps that went into the construction of a proof.

In the students' version of the software, exercises are served up with a theorem database and Derivation System rules tailored to the position in the course. In this version, however, the user will see the entire database at once, as well has having all Derivation System rules available.

The stand-alone version does not include the Maple libraries that are packaged with the EPGY Course System, so some Derivation System rules and verification strategies may not work correctly.

Proofs and databases

To view these proofs, save them to the folder containing the ProofEd.exe executable (probably c:\EPGY\Proof Environment).

To view most proofs correctly, will also need the correct theorem database; if a theorem's name does not appear in the open database, it will not appear in a justification line for any proof step, some some inferences may seem quite mysterious!

Linear Algebra

The "standard" theorem database for Linear Algebra proofs:

linalg.thdb

A proof that (AB)^T = B^TA^T for matrices A and B:

ex3.3.proof

A more detailed proof of the same fact:

ex3.4.proof

A proof that BB^T is symmetric for any square matrix B:

ex4.5.proof

A proof that eigenvectors with different eigenvalues are linearly independent, and the proof's special theorem database:

m51aEIGENVECTOR.proof, and m51aEIGENVECTOR.thdb

Geometry

The "standard" theorem database for Geometry proofs:

m015.thdb

Assume P and Q are distinct point; points A, B, and P are collinear; points A, B, and Q are collinear; and points P, Q, and R are collinear. Then A, B, and R are collinear:

ex3_1_7.proof

There exist two distinct lines:

ex3_2_3.proof

If point B is between point A and point C and point P is on both segment(A,B) and segment(B,C), then P=B:

ex3_4_4.proof

Guide

We have compiled a brief Users' Guide to the Theorem Proving Environment. This guide that is made available to our students to supplement the explanations given in the course. It is intended merely to document the features of the system rather than as a tutorial on using the program.

You may also download a ZIP archive containing the Guide, for viewing off-line.