Ask HN: For an automated theorem prover in prop. logic: Haskell or OCaml?

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.

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?