A Proof-Theoretic Approach to Logic Programming

Abstract

We introduce a definitional extension of logic programming by means of an inference schema (Ph), which, in acertain sense, is dual to the (1-P) schema of rule application discussed in Part I. In the operational semantics, this schema is dual to the resolution principle. We prove soundness and completeness for the extended system, discuss the computation of substitutions that this new schema gives rise to, and also consider the notion of negation intrinsic to the system and its relation to negation by failure.