A theorem prover is a dependently typed functional programming language. If you can generate a term with a particular type then the theorem is true. There is no testing involved.
It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed.
Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.
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.