This project is not in active development. For the successor, please see LogicPenguin (https://github.com/frabjous/logicpenguin).
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker
This is a demo of a proof checker for Fitch-style natural deduction systems found in many popular introductory logic textbooks, such as Barwise & Etchemendy's Language, Proof, and Logic or Bergmann & Moore's The Logic Book.
The specific system used here is the one found in forall x: Calgary Remix, by P. D. Magnus, Tim Button, J. Robert Loftis, Aaron Thomas-Bolduc and Richard Zach. It is based on forall x: an Introduction to Formal Logic, by P.D. Magnus. However, the proof system in the original version differs from the one used in the Calgary Remix.
See it in action at proofs.openlogicproject.org
To install, put the entire contents of this repository into a directory served to the web. It requires that your web server runs PHP 7+.
This code was originally written by Kevin C. Klement https://people.umass.edu/klement.
This project is not in active development. For the successor, please see LogicPenguin (https://github.com/frabjous/logicpenguin).