A Logic Programming System for Non-monotonic Reasoning

Research output: Contribution to journalArticlepeer-review

50 Citations (Scopus)


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 programs. 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 ofWFSX as the base semantics is justi-fied 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 ofWFSX, WFSX p , 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 inWESX p simply by detecting the violation of integrity rulesf L, -L introduced for eachL 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.
Original languageEnglish
Pages (from-to)93-147
Number of pages55
JournalJournal of Automated Reasoning
Issue number1
Publication statusPublished - Feb 1995


  • belief revision
  • well-founded semantics
  • logic programming
  • procedures
  • semantics
  • nonmonotonic reasoning


Dive into the research topics of 'A Logic Programming System for Non-monotonic Reasoning'. Together they form a unique fingerprint.

Cite this