Combining negation as failure and embedded implications in logic programs

In this paper we consider a language which combines embedded hypothetical implications and negation as failure (NAF). For this language we develop a top-down query evaluation procedure, a Kripke/Kleene fixed point semantics, and a logical interpretation by means of a completion construction. As a difference with respect to other proposals, we put no restriction on the occurrences of negation by failure; in particular, programs are not required to be stratified. The operational semantics we propose is an extension to our language of Stärk's ESLDNF, and allows 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 flat logic programs and makes use of Kleene strong three-valued logic. The completion of a program is a recursive theory interpreted in a three-valued modal logic. We prove soundness and completeness of the operational semantics with respect to both the fixed point semantics and the completion. While soundness results require no restriction, completeness results are limited by the possibility of floundering. Similarly to Stärk, we prove completeness for the class of so-called ∈-queries, which are not subjected to floundering. Since the property of being an ∈-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 flat programs.