There are many different ** Prolog**s 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.

Mon May 24 20:14:48 BST 1999