Transforming normal logic programs to constraint logic programs

A normal logic program P is transformed to another P^ω by a bottom-up computation on the positive component of P while the negative counterpart is left untouched. The declarative semantics of P is given by the completion of P^ω. The completed predicate definitions in P^ω, if they do not contain local variables, can be used as a basis for expanding each negated atom in the bodies of P^ω. We show that for a class of programs where every negative subgoal can be expanded, the resultant program P′ is a definite logic program with equality and disequality constraints. If the program falls outside this class, the resultant program may be executed using constructive negation. Our proposed scheme provides an effective sound and complete query-answering system for the well-founded models of a class of programs whose positive part has a finite P^ω and whose clauses satisfy the positive groundedness property defined herein.