Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 8, Issue 2: April 1998.

A note on SLDNF-resolution

W Buchholz

Mathematisches Institut, Universitat Munchen, Theresienstr. 39, D-80333 Munchen, Germany. E-mail: buchholz@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 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.

Pages 159-167

This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_02/080159.sgm.abs.html
Last modification: 4 June 1998.
Copyright© Oxford University Press, 1998.