An "interactive" Theorem Prover for First-order Logic
This is my attempt at building a small LCF-style theorem prover that is incomplete and most likely unsound.
The core syntax and semantics can be found in core.ml.
A string version (string variable/atom identifiers) can be found in string_prover.ml. There one can also find some
theorems and even a double negation elimination tactic.