🚀 go-pugleaf

The meaning is summed up in the first chapter ("declarative
semantics") on page 24 of the first edition of Lloyd's book.

It defines theta to be a correct answer substitution for
a program P and goal G if the universal closure of G theta
is a logical consequence of P (that is, all instances of
G theta are true in all models of P).

This definition is given before SLD resolution, the operational
semantics of Prolog, is discussed at all.  The basic semantics of
pure Prolog can be given without any operational concepts.  Most
functional languages and imperative languages have semantics based
on operational concepts such as reduction and assignment.  However,
this does not necessarily mean that declarative semantics do not
exist for such languages.  We should therefore be wary of calling
such languages non-declarative (or even non- logic programming).

Are difference lists (etc) a problem?  If you misunderstand them 
they are, otherwise they are not (after all, they are just terms).
Thinking that [1,2,3] \ [3] is the same as [1,2] is like thinking
that 3 - 1 is the same as 2.  The fact that some people get
expressions confused with numbers does not mean that expressions
cause a problem for the semantics of the language.

Is incompleteness a problem?  Unfortunately, there is not yet a
theorem prover implementation which is complete (you need an unbounded
amount of memory for a start).  One of important features of SLD
resolution is that queries with correct answers substitutions will
not finitely fail.  This means that negation as failure is sound.
In programming languages, as opposed to theorem proving systems,
we want to be able to specify algorithms and completeness is less
important.

	lee