a propositional theorem prover which uses Wang's algorithm (based on the sequent calculus LK). Provides a printout of the step-by-step proof and prints out the instance of failure in case the algorithm fails.
(final project for Computational Logic and Logic Programming at Wesleyan University, Fall 2014)