© 1998 by Oxford University Press
Original Articles |
A note on SLDNF-resolution
Mathematisches Institut, Universität München Theresienstr. 39, D-80333 München, Germany E-mail: buchholz{at}rz.mathematik.uni-muenchen.de
We introduce a new notion of SLDNF-tree and prove a completeness result for SLDNF-resolution that extends a theorem by Stä rk: 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