Created by Jesse Rappaport
Here you will find visualizations of automated proof methods in propositional and first-order logic. There are currently three available methods: tableaux proofs, truth tables, and resolution proofs. Currently, only tableaux proofs support first-order logic and quantification. (Quantified modal proofs are "constant-domain" proofs.) You will also find simple and clear information explaining each method, as well as some basic concepts in logic and modal logic.
This page is primarily intended as a teaching tool. The visualizations seek to replicate a manual proof, and the explanations are intended to be intuitive and not heavily technical. However, some background understanding of logic and proof methods may be required.
Please feel free to contact the author if you enjoy the program / find a bug or logical error / use this website in your class / have a question / have suggestions for improvement.