An interpreter for sentential logic (propositional calculus) written in Python. Includes a resolution-based automated theorem prover.