These pages describe writing an automated theorem prover from scratch as a hobbyist exercise. It is not done from an academic position, so theory is definitely given second place to praxis.

This theorem prover is implemented in Java rather than a language like OCAML. I know Java, and JetBrains’s IntelliJ IDEA IDE has been very helpful doing the development. This theorem prover does not follow or benefit from any other work on theorem proving out there.

This theorem prover is also far from finished, and in a constant state of flux. One of the nice things about a solo hobbyist project is one can rearrange the deck chairs as one pleases.