  In solving a query, the SLD proof procedure for definite programs sometimes
searches an infinite space for a non existing solution. For example, querying a
planner for an unreachable goal state. Such programs motivate the development
of methods to prove the absence of a solution. Considering the definite program
and the query ``<- Q'' as clauses of a first order theory, one can apply model
generators which search for a finite interpretation in which the program
clauses as well as the clause ``false <- Q'' are true. This paper develops a
new approach which exploits the fact that all clauses are definite. It is based
on a goal directed abductive search in the space of finite pre-interpretations
for a pre-interpretation such that ``Q'' is false in the least model of the
program based on it. Several methods for efficiently searching the space of
pre-interpretations are presented. Experimental results confirm that our
approach find solutions with less search than with the use of a first order
model generator.
