A definite clause is an -constraint of the form:
where 
, 
and q are atoms and
is an -constraint. We call q the head of a clause and
its body. We may write a clause as
or simply as 
. In case
the head and the body of a clause is empty, we call the clause an
empty clause. In general, an empty clause is of form
A definite clause specification is a set of definite clauses. Höhfeld and Smolka show that important properties of conventional logic programs extend to definite clause specifications, especially the existence of a unique minimal model for each interpretation in .
A goal is a possibly empty conjunction of -atoms and an -constraint, written as:
that is, a clause with an empty head (or consequent).
An S-answer to a goal with respect to a given definite specification
S is a satisfiable constraint , such that
is valid for every minimal model of
S.