The E Proof Checker (EPC) is a software program written in Java which verifies Euclidean-style diagrammatic proofs written in E, a formal system created by Jeremy Avigad, Edward Dean, and John Mumma of Carnegie Mellon University.
In a nutshell, the EPC allows you to supply simple text-based proofs using the construction rules of E and then view all the direct diagrammatic consequences as generated by the EPC using the inferences rules of E. For more information on the EPC program, the language of E, or the historical and philosophical underpinnings of this work please see my masters thesis.
Instructions
Installing the program should be very easy. If you have any problems, see the caveats or just shoot me an email.- Make sure you have Java installed on your computer.
- Download the EPC by clicking here.
- Open the downloaded file.
- Type in a proof in the first text area using the construction rules defined here.
- Click "Check" to validate the proof and view the entailments. That's it!
Simple Proof
Here's an example of a simple proof in E that can be parsed by the EPC:
Let L be a line.
Let a be a point on L.
Let b be a point on L distinct from a.
Let c be a point on L between a and b.
Let d be a point on L between a and c.
Hence d is between a and b.
Hence c is between a and b.
Partial Proof of Proposition I.1 from the Elements
Here's a proof in E of Proposition I.1 of the elements.
Let a be a point.
Let b be a point.
Let C be a circle with center a passing through b.
Let D be a circle with center b passing through a.
Let c be a point of intersection of C and D.
Have a b = a c.
Have b a = b c.
Comments and Caveats
- The source code is available here. Note that the program was developed using the Java programming language using the Eclipse IDE. It should be as easy as importing the project into your Eclipse workspace.
- If asked what program to open the download with, choose "javaws.exe" located in your JAVA_HOME/bin directory. Note: you may get a weird JScript error, but just ignore it)
- The user interface is extremely clunky! I whipped it up in an hour or so, but hope to make it a little better soon.
- Most of the prerequisites defined in E do work, although they give cryptic error messages when not met. The best way to debug is to refer to the original paper from Avigad, Mumma, and Dean. Typically they need "distinct" clauses to be added to previous sentences to assert that two elements are not equal.
- Performance for modest proofs should be reasonable (10-20 seconds), however more complex proofs can cause some churn (>1 minute). If the program seems to hang, it is still working. You can exit out if necessary.
- In general, error messages from the parser are relatively straight-forward, since they should give the line and character number of the problem.
- Demonstrations do work, but the exact language of a valid demonstration step is not well defined, so the best way to check if a relation was generated is (unfortunately) to manually inspect the entailments.
