N-Prolog and equivalence of logic programs

The aim of this work is to develop a declarative semantics for N-Prolog with negation as failure. N-Prolog is an extension of Prolog proposed by Gabbay and Reyle (1984, 1985), which allows for occurrences of nested implications in both goals and clauses. Our starting point is an operational semantics of the language defined by means of top-down derivation trees. Negation as finite failure can be naturally introduced in this context. A goal-G may be inferred from a database if every top-down derivation of G from the database finitely fails, i.e., contains a failure node at finite height.Our purpose is to give a logical interpretation of the underlying operational semantics. In the present work (Part 1) we take into consideration only the basic problems of determining such an interpretation, so that our analysis will concentrate on the propositional case. Nevertheless we give an intuitive account of how to extend our results to a first order language. A full treatment of N-Prolog with quantifiers will be deferred to the second part of this work.Our main contribution to the logical understanding of N-Prolog is the development of a notion of modal completion for programs, or databases. N-Prolog deductions turn out to be sound and complete with respect to such completions. More exactly, we introduce a natural modal three-valued logic PK and we prove that a goal is derivable from a propositional program if and only if it is implied by the completion of the program in the logic PK. This result holds for arbitrary programs. We assume no syntactic restriction, such as stratification (Apt et al. 1988; Bonner and McCarty 1990). In particular, we allow for arbitrary recursion through negation.Our semantical analysis heavily relies on a notion of intensional equivalence for programs and goals. This notion is naturally induced by the operational semantics, and is preserved under substitution of equivalent subexpressions. Basing on this substitution property we develop a theory of normal forms of programs and goals. Every program can be effectively transformed into an equivalent program in normal form. From the simple and uniform structure of programs in normal form one may directly define the completion.