
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

A Combination of SLDNF Resolution with Narrowing for General Logic Programs with Equations with Respect to Extended WellFounded Model
Susumu YAMASAKI Kazunori IRIYA
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E82D
No.10
pp.13031315 Publication Date: 1999/10/25 Online ISSN:
DOI: Print ISSN: 09168532 Type of Manuscript: PAPER Category: Automata,Languages and Theory of Computing Keyword: SLDNF resolution with infinite failure, narrowing, wellfounded model,
Full Text: PDF>>
Summary:
Negation as failure is realized to be combined with SLD resolution for general logic programs, where the combined resolution is called an SLDNF resolution. In this paper, we introduce narrowing and infinite failure to SLDNF resolution for general logic programs with equations. The combination of SLDNF resolution with narrowing and infinite failure is called an SLDNFN resolution. In Shepherdson (1992), equation theory is combined with SLDNF resolution so that the soundness may be guaranteed with respect to Clark's completion. Generalizing the method of Yamamoto (1987) for definite clause sets with equations, we formally define a least fixpoint semantics, which is an extension of Fitting (1985) and Kunen (1987) semantics, and which includes the pair of success and failure sets defined by the SLDNFN resolution. The relationship between the fixpoint semantics and the pair of sets is regarded as an extension of the relationships for general logic programs as in Marriott and et al. (1992) and in Yamasaki (1996). Instead of generalizing Clark's completion for SLDNFN resolution, we establish, as a model for general logic programs with equations, an extended wellfounded model so that the SLDNFN resolution is sound and complete for nonfloundering queries with respect to the extended wellfounded model.

