Proof Checker for forall x: Cambridge and Calgary

Kevin Klement has done up a prototype of his online natural deduction proof builder/checker that works with the natural deduction system of the Cambridge and Calgary versions of forall x.  The system was originally written for UMass’s Intro Logic course, based on Gary Hardegree’s online textbook. Kevin writes:

Earlier I mentioned making some online exercises for the “forall x” book. Not sure how far I’ll follow through with it, but I did go ahead and mock up a proof builder and checker, and sample exercises using them. That seems like the most fun/interesting part. I wasn’t intending to target the Calgary remix, but that’s the version I was looking at when I made it. I realized only later that the proof system and notation is different from the original, but I left it stand. Anyway, I thought I’d post a demo before taking it any further, so others can take a look, make suggestions, and help identify bugs. The user interface was the hardest part, and I’m not entirely happy with it as is, but not sure how to improve. Let me know what you think.

https://the21stcenturymonads.net/forallx/

If you find a bug or have suggestions for improvements, please let Kevin know! The code is open source (download link at the bottom of the page).

UPDATE: The code is now on GitHub and runs on proofs.openlogicproject.org

1 comment

  1. Logic Courseware? – Richard Zach

    […] backend code for all of this is available and could be adapted to your own needs. He has provided a version of the proof checker that works with the Cambridge and Calgary versions of forall x, and that code is open source, […]

Comments are closed.