## Abstract

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 of*WFSX* 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 of*WFSX, 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 in*WESX*
_{
p
} simply by detecting the violation of integrity rules**f** ←*L*, -*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.

This is a preview of subscription content, log in to check access.

## References

- 1.
Alferes, J. J., Damásio, C. V., and Pereira, L. M.: SLX—A top-down derivation procedure for programs with explicit negation, in M. Bruynooghe (ed.),

*ILPS, MIT Press*, 1994 (to appear). - 2.
Alferes, J. J., Damásio, C. V., and Pereira, L. M.: Top-down query evaluation for well-founded semantics with explicit negation, in A. Cohn (ed.),

*Proc. ECAI'94*, Morgan Kaufmann, 1994, pp. 140–144. - 3.
Alferes, J. J. and Pereira, L. M.: On logic program semantics with two kinds of negation, in K. Apt (ed.),

*Int. Joint Conf. and Symp. on LP*, MIT Press, 1992, pp. 574–588. - 4.
Alferes, J. J. and Pereira, L. M.: Belief, provability, and logic programs, in C. MacNish, D. Pearce, and L. M. Pereira (eds),

*JELIA'94*, Lecture Notes in AI 838 (798), Springer-Verlag, 1994, pp. 106–121. - 5.
Alferes, J. J. and Pereira, L. M.: Contradiction: When avoidance equals removal, in R. Dyckhoff (ed.),

*4th Int. Ws. on Extensions of LP*, Lecture Notes in AI 839 (798), Springer-Verlag, 1994. - 6.
Alferes, José Júlio:

*Semantics of Logic Programs with Explicit Negation*, Ph.D. Thesis, Universidade Nova de Lisboa, 1993. - 7.
Apt, K. and Bol, R.: Logic programming and negation: A survey,

*J. Logic Programming***19/20**(1994), 9–72. - 8.
Apt, K., Bol, R., and Klop, J.: On the safe termination of Prolog programs, in Levi and Marteli (eds),

*Proc. LCLP'89*, MIT Press, 1989, pp. 353–368. - 9.
Baral, C. and Gelfond, M.: Logic programming and knowledge representation,

*J. Logic Programming***19/20**(1994), 73–148. - 10.
Bidoit, N. and Legay, P.: Well!: An evaluation procedure for all logic programs, in

*Int. Conf. on Database Technology*, 1990, pp. 335–348. - 11.
Bol, R. and Degerstedt, L.: Tabulated resolution for well founded semantics, in

*Proc, ILPS'93*, MIT Press, 1993. - 12.
Chen, W. and Warren, D. S.: A goal-oriented approach to computing well-founded semantics, in K. Apt (ed.),

*Int. Joint Conf. on Logic Programming*, MIT Press, 1992, pp. 589–603. - 13.
Chen, W. and Warren, D. S.: Query evaluation under the well founded semantics, in

*PODS'93*, 1993. - 14.
Chou, T. S.-C. and Winslett, M.: A model-based belief revision system,

*Journal of Automated Reasoning***12**(2) (1994), 157–208. - 15.
Clark, K.: Negation as failure, in H. Gallaire and J. Minker (eds),

*Logic and Data Bases*, Plenum Press, 1978, pp. 293–322. - 16.
Colmerauer, A., Kanoui, H., Roussel, P., and Pasero, R.: Un systéme de communication hommemachine en français. Technical report, Groupe de Recherche en Intelligence Artificielle, Université d'Aix-Marseille II, 1973.

- 17.
Dalal, M.: Investigations into a theory of knowledge base revision: Preliminary report, in

*7th AAAI*, 1988, pp. 475–479. - 18.
Damásio, C. V., Nejdl, W., and Pereira, L. M.: REVISE: An extended logic programming system for revising knowledge bases, in

*KR'94*, Morgan Kaufmann, 1994. - 19.
Denecker, M. and De Schreye, D.: SLDNFA: An abductive procedure for normal abductive programs, in K. Apt (ed.),

*Int. Joint Conf. and Symp. on LP*, MIT Press, 1992, pp. 686–700. - 20.
Dix, J.: Classifying semantics of logic programs, in A. Nerode, W. Marek, and V. S. Subrahmanian (eds),

*LP & NMR*, MIT Press, 1991, pp. 166–180. - 21.
Dix, J.: A framework for representing and characterizing semantics of logic programs, in B. Nebel, C. Rich, and W. Swartout (eds),

*KR'92*, Morgan Kaufmann, 1992. - 22.
Dung, P. M.: Negation as hypotheses: An abductive framework for logic programming, in K. Furukawa (ed.),

*8th Int. Conf. on LP*, MIT Press, 1991, pp. 3–17. - 23.
Eshghi, K. and Kowalski, R.: Abduction compared with negation by failure, in

*Proc. 6th Int. Conf. on LP*, MIT Press, 1989. - 24.
Van Gelder, A., Ross, K. A., and Schlipf, J. S.: The well-founded semantics for general logic programs,

*Journal of the ACM***38**(3) (1991), 620–650. - 25.
Gelfond, M. and Lifschitz, V.: The stable model semantics for logic programming, in R. Kowalski and K. A. Bowen (eds),

*5th Int. Conf. on LP*, MIT Press, 1988, pp. 1070–1080. - 26.
Gelfond, M. and Lifschitz, V.: Compiling circumscriptive theories into logic programs, in M. Reinfrank, J. de Kleer, M. Ginsberg, and E. Sandewall (eds),

*2nd Int. Ws.on NMR*, LNAI 346, Springer-Verlag, 1989, pp. 74–99. - 27.
Gelfond, M. and Lifschitz, V.: Logic programs with classical negation, in Warren and Szeredi (eds),

*Proc. 7th Int. Conf. on LP*, MIT Press, 1990, pp. 579–597. - 28.
Gelfond, M. and Lifschitz, V.: Representing actions in extended logic programs, in K. Apt (ed.),

*Int. Joint Conf. and Symp. on LP*, MIT Press, 1992, pp. 559–573. - 29.
HMSO:

*British Nationality Act*, Her Majesty's Stationery Office, 1981. - 30.
Kakas, A. C. and Mancarella, P.: Generalized stable models: A semantics for abduction, in

*Proc. ECAI'90*, 1990, pp. 401–405. - 31.
Katsuno, H. and Mendelzon, A. O.: On the difference between updating a knowledge base revising it, in J. A. Allen

*et al.*(eds),*2nd KRR*, Morgan Kaufmann, 1991, pp. 387–394. - 32.
Kemp, D. B., Stuckey, P. J., and Srivastava, D.: Query restricted bottom-up evaluation of normal logic programs, in

*Proc. JICSLP'92*, MIT Press, 1992, pp. 288–302. - 33.
Kowalski, R.:

*Logic for Problem Solving*, North Holland, 1978. - 34.
Kowalski, R.: The treatment of negation in logic programs for representing legislation, in

*2nd Int. Conf. on AI and Law*, 1989, pp. 11–15. - 35.
Kowalski, R.: Problems and promises of computational logic, in John Lloyd (ed.),

*Computational Logic*, Basic Research Series, Springer-Verlag, 1990, pp. 1–36. - 36.
Kowalski, R.: Legislation as logic programs, in

*Logic Programming in Action*, Springer-Verlag, 1992, pp. 203–230. - 37.
Kowalski, R. and Khuener, D.: Linear resolution with selection function,

*Artificial Intelligence***5**(1971), 227–260. - 38.
Kraus, S., Lehmann, D., and Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics,

*Artificial Intelligence***44**(1990), 167–207. - 39.
Kunen, K.: Negation in logic programming,

*Journal of Logic Programming***4**(1987), 289–308. - 40.
Lloyd, J.: Declarative error diagnosis,

*New Generation Computing***5**(2) (1987). - 41.
Lloyd, J.:

*Foundations of Logic Programming*, Springer-Verlag, 1987. - 42.
Lloyd, J. and Topor, R.: A basis for deductive database systems,

*Journal of Logic Programming*,**2**(1985), 93–109. - 43.
Nebel, B.: Syntax based approaches to belief revision, in: P. Gärdenfors (ed.),

*Belief Revision*, Cambridge University Press, 1992, pp. 52–88. - 44.
Pearce, D. and Wagner, G.: Reasoning with negative information I: Strong negation in logic programs, in L. Haaparanta, M. Kusch, and I. Niiniluoto (eds),

*Language, Knowledge and Intentionality*, Acta Philosophica Fennica 49, 1990, pp. 430–453. - 45.
Pereira, L. M. and Alferes, J. J.: Well founded semantics for logic programs with explicit negation, in B. Neumann (ed.),

*European Conf. on AI*, John Wiley & Sons, 1992, pp. 102–106. - 46.
Pereira, L. M., Alferes, J. J., and Aparicio, J. N.: Contradiction removal within well founded semantics, in A. Nerode, W. Marek, and V. S. Subrahmanian (eds),

*LP & NMR*, MIT Press, 1991, pp. 105–119. - 47.
Pereira, L. M., Aparicio, J. N., and Alferes, J. J.: A derivation procedure for extended stable models, in

*Int. Joint Conf. on AI*, Morgan Kaufmann, 1991. - 48.
Pereira, L. M., Aparicio, J. N., and Alferes, J. J.: Non-monotonic reasoning with logic programming,

*Journal of Logic Programming. Special issue on Nonmonotonic Reasoning*,**17**(2–4) (1993), 227–263. - 49.
Pereira, L. M., Damásio, C., and Alferes, J. J.: Debugging by diagnosing assumptions, in P. A. Fritzson (ed.),

*1st Int. Workshop on Automatic Algorithmic Debugging, AADEBUG'93*, LNCS, vol. 749, Springer-Verlag, 1993, pp. 58–74. - 50.
Pereira, L. M., Damásico, C., and Alferes, J. J.: Diagnosis and debugging as contradiction removal, in L. M. Pereira and A. Nerode (eds),

*2nd Int. Workshop on Logic Programming & NMR*, MIT Press, 1993, pp. 316–330. - 51.
Pereira, L. M., Damásio, C., and Alferes, J. J.: Diagnosis and debugging as contradiction removal in logic programs, in L. Damas and M. Filgueiras (eds),

*6th Portuguese AI Conf.*, Springer-Verlag, 1993. - 52.
Gärdenfors, P.:

*Knowledge in Flux: Modeling the Dynamics of Epistemic States*, The MIT Press, 1988. - 53.
Przymusinska, H., Przymusinski, T. C., and Seki, H.: Soundness and completeness of partial deductions for well-founded semantics, in A. Voronkov (ed.),

*Proc. of the Int. Conf. on Automated Reasoning*, LNAI 624, 1992. - 54.
Przymusinski, T.: Every logic program has a natural stratification and an interated fixed point model, in

*8th Symp. on Principles of Database Systems*, ACM SIGACT-SIGMOD, 1989. - 55.
Przymusinski, T.: Extended stable semantics for normal and disjunctive programs, in Warren and Szeredi (eds),

*7th Int. Conf. on LP*, MIT Press, 1990, pp. 459–477. - 56.
Przymusinski, T.: Static semantics for normal and disjunctive programs, Technical report, Dept. of Computer Science, Univ. of California at Riverside, 1993.

- 57.
Przymusinski, T. and Warren, D. S.: Well-founded semantics: Theory and implementation, 1992.

- 58.
Reiter, R.: On closed-world data bases, in H. Gallaire and J. Minker (eds),

*Logic and Data Bases*, Plenum Press, 1978, pp. 55–76. - 59.
Reiter, R.: Towards a logical reconstruction of relational database theory, in M. Brodie, and J. Mylopoulos (eds),

*On Conceptual Modelling*, Springer-Verlag, 1984, pp. 191–233. - 60.
Reiter, R.: On asking what a database knows, in John Lloyd (ed.),

*Computational Logic*, Basic Research Series, Springer-Verlag, 1990, pp. 96–113. - 61.
Ross, K. A.: A procedural semantics for well-founded negation in logic programs,

*Journal of Logic Programming***13**(1992), 1–22. - 62.
Teusink, F.: A proof procedure for extended logic programs, in

*Proc. ILPS'93*, MIT Press, 1993. - 63.
Van Gelder, A.: The alternating fixpoint of logic programs with negation, in

*Proc. of the Symposium on Principles of Database Systems*, ACM SIGACT-SIGMOD, 1989, pp. 1–10. - 64.
Wagner, G.: A database needs two kinds of negation, in B. Thalheim, J. Demetrovics and H.-D. Gerhardt (eds),

*Mathematical Foundations of Database Systems*, LNCS 495, Springer-Verlag, 1991, pp. 357–371. - 65.
Wagner, G.: Logic programming with strong negation and innexact predicates,

*J. of Logic and Computation***1**(6) (1991), 835–861. - 66.
Wagner, G.: Neutralization and preemption in extended logic programs, Technical report, Freien Universitat, Berlin, 1993.

- 67.
Wagner, G.: Reasoning with inconsistency in extended deductive databases, in L. M. Pereira and A. Nerode (eds),

*2nd Int. Ws. on LP & NMR*, MIT Press, 1993, pp. 300–315. - 68.
Winslett, M.: Reasoning about action using a possible model approach, in

*7th AAAI*, 1988, pp. 89–93.

## Author information

### Affiliations

## Rights and permissions

## About this article

### Cite this article

Alferes, J.J., Damásio, C.V. & Pereira, L.M. A logic programming system for nonmonotonic reasoning.
*J Autom Reasoning* **14, **93–147 (1995). https://doi.org/10.1007/BF00883931

Received:

Issue Date:

### Key words

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