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 concatenate/3, then the declarative semantics tells us
that
?- concatenate([a], [b], [a,b]).
is true, because this goal is the head of a certain instance
of the first clause for concatenate/3, namely,
concatenate([a], [b], [a,b]) :- concatenate([], [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 that is the second clause for concatenate/3.