There are many different Prologs but they are all based on a technique from theorem proving known as SLD Resolution.
SLD resolution can be guaranteed to be complete in that if a solution exists then it can be found using some search strategy.
SLD resolution can be guaranteed to be sound in that if an answer is obtained then it is a solution to the original problem for some search strategy.
It is a research goal to study Prolog implementations and check that their search strategy preserves the completeness and soundness of the underlying method of SLD resolution.
Note that the cut can affect completeness but not soundness.
Note also that there is no theoretical way of determining whether or not an attempt to solve a problem will terminate. If there is a solution then it can be shown that it can be found in a finite number of steps.