Propositonal Logic Prover written in Ocaml. To compile
ocamlc -I +labltk labltk.cmagraphics.cma plp.ml -o plp
or
ocamlc -I +labltk labltk.cma graphics.cma plp.ml -o plp
Proving simple logical formula (p→q)→(-q →-p) in classical propositional logic.