Logic Tools

Free software for learning symbolic logic, written to accompany How Logic Works but usable with any course that teaches natural deduction in the Lemmon style. Nothing to install, no account, no charge.

Open the tools →

Check a proof you wrote by hand

Photograph a completed proof with your phone and the page is transcribed and checked. You see the transcription beside the photograph and correct it before anything is judged, so a misreading costs you an edit rather than a wrong answer.

Check a proof you type

Enter a derivation line by line and every line is checked against the rules: the dependencies, the citations, and the rule itself. When a line fails you are told which requirement it missed, not merely that something is wrong.

Sentences, truth tables and models

For instructors

The proof checker implements the twenty-one rules of How Logic Works exactly as the book states them, including the dependency bookkeeping that most software omits. It is deliberately strict about citation order and about blank dependency cells, because those are where students’ mistakes actually live.

Students need no account and submit nothing to me; the tools run in the browser against a small server and keep no record of what is checked. You are welcome to link to any of these pages from a syllabus.

The whole suite is open source and written in Haskell. If your course uses a different rule set, the checker is small enough to adapt.