"Is Prolog a theorem prover? Richard O'Keefe said it best:

    Prolog is an efficient programming language because it is a very stupid theorem prover."

Who am I to overrule the author of The Craft of Prolog?

Some would say that SLDNF resolution qualifies as theorem proving, some would disagree and say that a theorem prover also needs such and such capability. Anyway, as Triska shows above you can implement software that is quite a lot like a theorem prover in about thirty lines of Prolog, i.e. not "a dependently typed functional programming language".

The descendants of Milner's work, notably ML and the Edinburgh LCF theorem prover, have been quite successful, though.