A LOGIC PROGRAMMING SYSTEM FOR NONMONOTONIC REASONING

The evolution of logic programming semantics has included the introduction of a new explicit form of negation, beside the older implicit (or default) negation typical of logic programming. The richer language has been shown adequate for a spate of knowledge representation and reasoning forms. The widespread use of such extended programs requires the definition of a correct top-down querying mechanism, much as for Prolog wrt. normal pro,srams. One purpose of this paper is to present and exploit a SLDNF-like derivation procedure, SLX, for programs with explicit negation under well-founded semantics (WFSX) and prove its soundness and completeness. (Its soundness wrt. the answer-sets semantics is also shown.) Our choice of WFSX as the base semantics is justified by the structural properties it enjoys, which are paramount for top-down query evaluation. Of course, introducing explicit negation requires dealing with contradiction. Consequently, we allow for contradiction to appear, and show moreover how it can be removed by freely changing the truth-values of some subset of a set of predefined revisable literals. To achieve this, we introduce a paraconsistent version of WFSX, WFSX,, that allows contradictions and for which our SLX top-down procedure is proven correct as well. This procedure can be used to detect the existence of pairs of complementary literals in WESX(p) simply by detecting the violation of integrity rules f double left arrow L, inverted right perpendicular L introduced for each L in the language of the program. Furthermore, integrity constraints of a more general form are allowed, whose violation can likewise be detected by SLX. Removal of contradiction or integrity violation is accomplished by a variant of the SLX procedure that collects, in a formula, the alternative combinations of revisable literals' truth-values that ensure the said removal. The formulas, after simplification, can then be satisfied by a number of truth-values changes in the revisable, among ''true,'' ''false'', and ''undefined''. A notion of minimal change is defined as well that establishes a closeness relation between a program and its revisions. Forthwith, the changes can be enforced by introducing or deleting program rules for the revisable literals. To illustrate the usefulness and originality of our framework, we applied it to obtain a novel logic programming approach, and results, in declarative debugging and model-based diagnosis problems.