from ref :
Is Prolog a theorem prover? Richard O'Keefe said: "Prolog is an efficient programming language because it is a very stupid theorem prover".
Thus, there is a connection between Prolog and theorem proving. In fact, execution of a Prolog program can be regarded as a special case of resolution, called SLDNF resolution.
However, Prolog is not a full-fledged theorem prover. In particular, Prolog is logically incomplete due to its depth-first search strategy: Prolog may be unable to find a resolution refutation even if one exists.