E Proof Checker


(2 comments)
May 19th 2011


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.
  1. Make sure you have Java installed on your computer.
  2. Download the EPC by clicking here.
  3. Open the downloaded file.
  4. Type in a proof in the first text area using the construction rules defined here.
  5. 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

  1. 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.
  2. 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)
  3. The user interface is extremely clunky! I whipped it up in an hour or so, but hope to make it a little better soon.
  4. 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.
  5. 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.
  6. In general, error messages from the parser are relatively straight-forward, since they should give the line and character number of the problem.
  7. 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.
I'm an "old" programmer who has been blogging for almost 20 years now. In 2017, I started Highline Solutions, a consulting company that helps with software architecture and full-stack development. I have two degrees from Carnegie Mellon University, one practical (Information and Decision Systems) and one not so much (Philosophy - thesis here). Pittsburgh, PA is my home where I live with my wife and 3 energetic boys.
I recently released a web app called TechRez, a "better resume for tech". The idea is that instead of sending out the same-old static PDF resume that's jam packed with buzz words and spans multiple pages, you can create a TechRez, which is modern, visual, and interactive. Try it out for free!
Got a Comment?
Comments (2)
shekhar
October 06, 2016
Let C be a circle with center a passing through b.

here do you mean E be a circle? instead C?
Olivier
October 07, 2016
Apparently the last line of the first proof is incorrect:
> Hence c is between a and b.
This is just equivalent to the 4th line:
> Let c be a point on L between a and b.
So I think the last line should be:
> Hence c is between d and b.