I was wondering what, if any, was the connection between prolog and theorem provers: https://www.metalevel.at/prolog/theoremproving

I doubt there is much of a connection. Prolog programs don't have any termination guarantees, so you can't use them to prove any theorems (since a program is supposed to correspond to a proof, but a non-terminating program is a proof with a big hole in it).

@Nick Smith The linked article jumps right at it by implementing "the resolution calculus for propositional logic" and "_not_ using Prolog's built-in search strategy as the search strategy of the prover!" So @Emmanuel Oga, I'd say that riska has a great grasp of what is at issue. I'm going to have to read his book https://www.metalevel.at/prolog.

Yes, but that’s not using the Prolog language as a theorem prover, that’s writing a theorem-proving DSL in Prolog, right? Huge difference.