Abstract

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, 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 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