A Combination of SLDNF Resolution with Narrowing for General Logic Programs with Equations with Respect to Extended Well-Founded Model

Susumu YAMASAKI  Kazunori IRIYA  

IEICE TRANSACTIONS on Information and Systems   Vol.E82-D   No.10   pp.1303-1315
Publication Date: 1999/10/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Automata,Languages and Theory of Computing
SLDNF resolution with infinite failure,  narrowing,  well-founded model,  

Full Text: PDF>>
Buy this Article

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 well-founded model so that the SLDNFN resolution is sound and complete for non-floundering queries with respect to the extended well-founded model.