Tight, consistent, and computable completions for unrestricted logic programs

Clark's program completion offers an intuitive first-order semantics for logic programs. Unfortunately, it does not fully capture the "tight" bottom- up semantics for recursive programs since it does not express enough negative information. Therefore, various canonical model semantics have been proposed which offer the required tight semantics for increasingly general classes of programs. Canonical models are defined in terms of fixpoint operators on program interpretations. The resulting semantics is hard to specify, harder to understand, and impossible to compute. In this paper, we propose to rehabilitate the program completion. We show how it can be extended to capture the tight semantics, and how a consistent completion can be derived for all programs, without resorting to three-valued logic. Finally, by lifting the restriction to Herbrand domains, we exhibit a tight, consistent, computable semantics for unrestricted logic programs. As with any completion, the meaning of a program is a set of axioms directly constructed from the program text.