\(N\)-Prolog and equivalence of logic programs. I (Q1314280)

The aim of this long paper is to introduce a declarative semantics for N- Prolog with negation as failure -- the extensions of Prolog proposed by Gabbay and Reyle, in which one allows occurrences of nested implications both in goals and in clauses. In N-Prolog, the intuitionistic deduction theorem gives the operational meaning of the goal ``D implies G'' by the stipulation that the goal succeeds from a program P iff G succeeds from P augmented by the data of D. Adding negation as failure to N-Prolog one obtains a powerful language which is well suited to perform some important meta-level constructs in the object language, and to introduce several structuring mechanisms in logic programming. As is well known, the language with hypothetical implication but without negation as failure can be logically interpreted in the context of intuitionistic logic: whenever P is a positive program, and G is a positive goal, we have that ``P?G'' succeeds iff G is intuitionistically derivable from P. On the other hand, by adding negation as failure, such properties as modus ponens no longer hold, and implication becomes pathological. In their paper the authors prove that N-Prolog deductions are sound and complete with respect to a certain notion -- developed in the same paper -- of modal completion of programs. Using a modal extension PK of Lukasiewicz three-valued logic, it is proved that a goal is derivable from a propositional program P iff in PK the goal is implied by the modal completion of P. No syntactic restrictions, such as stratification, are assumed. The semantical analysis of N-Prolog deductions relies on the notion of intensional equivalence for programs and goals. Starting from the notion of substitution underlying intensional equivalence, the authors develop a theory of normal forms of programs and goals; they show that every program P can be effectively transformed into an equivalent program \(\text{P}'\) in normal form. Once P is reduced to \(\text{P}'\), the completion of P can be straightforwardly constructed from the simple and uniform structure of \(\text{P}'\). In the final part of their paper, the authors give some indication on how to extend their constructions to the first-order case.