gentzen An automated theorem prover for propositional logic, written in OCaml. To be written for the web!