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 which is the second
clause for concatenate/3.