Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 9, Issue 1, pp. 47-61: Abstract.

A direct proof of the completeness of SLDNF-resolution

R Stärk

Institute of Informatics, University of Fribourg, Rue Faucigny 2, CH-1700 Fribourg, Switzerland. E-mail: robert.staerk@unifr.ch

We give a direct proof of the following theorem: if a goal G[sgr] is a logical consequence of the partial completion of an arbitrary normal logic program P, then each fair, non-floundering SLDNF-tree T for G yields an answer substitution &thgr which is more general than [sgr]. If the negation G is a logical consequence of the partial completion of P, then T is finitely failed. A tree is fair, if each negative main branch ends in failure or each literal in the branch is selected at a certain point. A tree is floundering if it contains a positive node that consists of negative, non-ground literals only.

Key words: Logic programming, negation as failure, SLDNF-resolution.

  Full-Text PDF  (283 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 1999.