A Combination of SLDNF Resolution with Narrowing for General Logic Programs with Equations with Respect to Extended Well-Founded Model
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 well-founded model so that the SLDNFN resolution is sound and complete for non-floundering queries with respect to the extended well-founded model.
- Publication
- IEICE TRANSACTIONS on Information Vol.E82-D No.10 pp.1303-1315
- Publication Date
- 1999/10/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Automata,Languages and Theory of Computing
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Susumu YAMASAKI, Kazunori IRIYA, "A Combination of SLDNF Resolution with Narrowing for General Logic Programs with Equations with Respect to Extended Well-Founded Model" in IEICE TRANSACTIONS on Information,
vol. E82-D, no. 10, pp. 1303-1315, October 1999, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e82-d_10_1303/_p
Copy
@ARTICLE{e82-d_10_1303,
author={Susumu YAMASAKI, Kazunori IRIYA, },
journal={IEICE TRANSACTIONS on Information},
title={A Combination of SLDNF Resolution with Narrowing for General Logic Programs with Equations with Respect to Extended Well-Founded Model},
year={1999},
volume={E82-D},
number={10},
pages={1303-1315},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={October},}
Copy
TY - JOUR
TI - A Combination of SLDNF Resolution with Narrowing for General Logic Programs with Equations with Respect to Extended Well-Founded Model
T2 - IEICE TRANSACTIONS on Information
SP - 1303
EP - 1315
AU - Susumu YAMASAKI
AU - Kazunori IRIYA
PY - 1999
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E82-D
IS - 10
JA - IEICE TRANSACTIONS on Information
Y1 - October 1999
AB - 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.
ER -
English
