COMBINING NEGATION AS FAILURE AND EMBEDDED IMPLICATIONS IN LOGIC PROGRAMS

In this paper we consider a language which combines embedded hypotheti cal implications and negation as failure (NAF). For this language we d evelop a top-down query evaluation procedure, a Kripke/Kleene fixed po int semantics, and a logical interpretation by means of a completion c onstruction. As a difference with respect to other proposals, we put n o restriction on the occurrences of negation by failure; in particular , programs are not required to be stratified. The operational semantic s we propose is an extension to our language of Stark's ESLDNF, and al lows negative non-ground literals to be selected in a query. The fixed point semantics is a generalization of those developed by Fitting and Kunen for fat logic programs and makes use of Kleene strong three-val ued logic. The completion of a program is a recursive theory interpret ed in a three-valued modal logic. We prove soundness and completeness of the operational semantics with respect to both the fixed point sema ntics and the completion. While soundness results require no restricti on, completeness results are limited by the possibility of floundering . Similarly to Stark, we prove completeness for the class of so-called epsilon-queries, which are not subjected to floundering. Since the pr operty of being an epsilon-query is undecidable, we give a syntactical decidable condition which ensures this property. Such a condition is a non-trivial generalization of the usual allowedness condition for fl at programs. (C) 1998 Elsevier Science Inc. All rights reserved.