|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 8, Issue 2: April 1998.
A note on SLDNF-resolution
Mathematisches Institut, Universitat Munchen, Theresienstr. 39, D-80333 Munchen, Germany. E-mail: firstname.lastname@example.org
We introduce a new notion of SLDNF-tree and prove a completeness result for SLDNF-resolution that extends a theorem by Stark: not only the existence of some successful (finitely failed, resp.) SLDNF-tree is established, but it is shown that every fair SLDNF-tree is successful (finitely failed, resp.).
Keywords: Logic programming, negation as failure, SLDNF-resolution.