The  semantics of definite clauses should be fairly clear from the informal
interpretations  already  given.   However  it  is useful to have a precise
definition.   The  declarative semantics of definite clauses tells us which
goals  can  be considered true according to a given program, and is defined
recursively as follows.

A  goal  is  true if it is the head of some clause instance and each of the
goals  (if  any)  in  the  body  of  that clause instance is true, where an
instance  of  a  clause  (or term) is obtained by substituting, for each of
zero  or  more  of  its  variables,  a  new term for all occurrences of the
variable.


For  example,  if  a program contains the preceding procedure for 'append',
then the declarative semantics tells us that:-

                             append([a],[b],[a,b])

is  true,  because this goal is the head of a certain instance of the first
clause for 'append', namely,

                  append([a],[b],[a,b]) :- append([],[b],[b]).

and we know that the only goal in the body of this clause instance is true,
since  it  is an instance of the unit clause which is the second clause for
'append'.

Note that the declarative semantics makes no reference to the sequencing of
goals  within the body of a clause, nor to the sequencing of clauses within
a  program.  This sequencing information is, however, very relevant for the
procedural   semantics   which  Prolog  gives  to  definite  clauses.   The
procedural  semantics  defines exactly how the Prolog system will execute a
goal,  and  the  sequencing  information  is  the means by which the Prolog
programmer  directs  the  system  to execute his program in a sensible way.
The  effect  of  executing  a  goal  is  to enumerate, one by one, its true
instances.    Here  then  is  an  informal  definition  of  the  procedural
semantics.

To  execute  a  goal,  the  system searches for the first clause whose head
matches  or unifies with the goal.  The unification process [Robinson 1965]
finds the most general common instance of the two terms, which is unique if
it  exists.   If  a  match  is  found, the matching clause instance is then
activated  by  executing in turn, from left to right, each of the goals (if
any)  in  its  body.  If at any time the system fails to find a match for a
goal,  it  backtracks,  ie.  it rejects the most recently activated clause,
undoing  any  substitutions  made by the match with the head of the clause.
Next  it reconsiders the original goal which activated the rejected clause,
and tries to find a subsequent clause which also matches the goal.

For example, if we execute the goal expressed by the question:-

                              append(X,Y,[a,b]) ?

we  find  that it matches the head of the first clause for 'append', with X
instantiated  to  [a, ..X1].  The new variable X1 is constrained by the new
goal produced, which is the recursive procedure call:-

                                append(X1,Y,[b])

Again  this  goal  matches the first clause, instantiating X1 to [b, ..X2],
and yielding the new goal:-

                               append(X2, Y, [])

Now  this goal will only match the second clause, instantiating both X2 and
Y  to  [].   Since  there  are  no  further goals to be executed, we have a
solution:-

     X = [a, b]
     Y = []

ie.  a true instance of the original goal is:-

                           append([a, b], [], [a, b])

If  this  solution  is  rejected,  backtracking  will  generate the further
solutions:-

     X = [a]
     Y = [b]

     X = []
     Y = [a,b]

in  that  order,  by  re-matching,  against the second clause for 'append',
goals already solved once using the first clause.
