Fully declarative logic programming

Abstract

In this paper we present a theoretical basis for implementation of a fully declarative logic programming language which allows use of quantifiers and negation in the statement bodies. We formulate SLPG - a resolution system extending SLD-resolution, but alternative to SLDNF. SLPG computes over an open universe of terms. It is complete for the full class of positive programs (with statements A ← B where B involves ⊤, ⊥, ⋀, ⋁, ∀, ∃, =), and also for a class of programs involving negative information in the form of guards (i.e. inequations between terms.) By augmenting SLPG with a mechanism of constructive negation we obtain SLPGCN-resolution which is complete for broader classes of programs involving negation - (without assuming any notion of stratification.).