Title says it all. I&#x27;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&#x27;d like to also output to LaTeX, but not so important.<p>I don&#x27;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?
Ask HN: For an automated theorem prover in prop. logic: Haskell or OCaml?