Title says it all. I'd like to write a program that, some givens and a theorem, can generate a Fitch-style proof of the theorem (not just a truth table). I'd like to also output to LaTeX, but not so important.<p>I don't know either Haskell or OCaml, and I thought I should learn one of them for this project. I already know Python and Clojure - any suggestions?