A backward chaining resolution process involving non-monotonic operators

  • D. Ferney
  • A. Quilliot
Non Monotonic Reasoning
Part of the Lecture Notes in Computer Science book series (LNCS, volume 682)


From a reflexion about the possible semantics of a special subset of the first order logic we extract a resolution process based upon dynamic handling through backward chaining of temporary knowledge. It leads us to the conception of an experimental declarative language, aimed at describing logical specifications, which unifies backward and forward chaining and makes easier dealing with a non monotonic behaviour of the knowledge.


“Suppose” operator Non monotonicity Resolution process 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi, Z. Manna: Modal theorem proving. Proc 8th Int Conf Automated deduction, Springer-Verlag LNCS 230, pp. 172–189 (1986).Google Scholar
  2. 2.
    K. Apt, M. Van Emden: Contributions to the theory of logic programming. JACM 29.3, pp. 941–862 (1982).Google Scholar
  3. 3.
    P. Besnard, P. Siegel: A framework for logic of “suppose” and “admit”. Proc JELIA 88 ROSCOFF (1988).Google Scholar
  4. 4.
    W. Bledsoe: Non resolution theorem proving; A.I. 9, pp. 1–35 (1977).Google Scholar
  5. 5.
    G. Bossu, P. Siegel: Saturation,non monotonic reasoning and the closed world assumption. A. I. 25(1) pp.13–65 (1985).Google Scholar
  6. 6.
    K. Bowen, T. Weinberg: A metalevel extension of PROLOG. Symp of logic Programing;BOSTON pp 48–53 (1985).Google Scholar
  7. 7.
    B. Chellas: Modal logic: an introduction. Cambrige Univ Press (1980).Google Scholar
  8. 8.
    A. Colmerauer, H. Kanoui, M. Van Caneghem: PROLOG: bases théoriques, développements actuels. TSI 2, 4 pp 271–313 (1983).Google Scholar
  9. 9.
    R. Davis: Reasoning about rules. A.I. 15, pp 223–239 (1980).Google Scholar
  10. 10.
    W. Dowling, J.H. Gallier: Linear time algorithms for testing the satisfiability of propositional Horn formulae. Jour Log Prog 1 (1984).Google Scholar
  11. 11.
    B. Fade: ARGOS II: Contribution à la réalisation d'un resolveur automatique de problèmes. Thèse de 3∘ cycle. Univ P.Sabatier Toulouse (1980).Google Scholar
  12. 12.
    M. Fitting: Proof methods for modal and intuitionistic logic. Reidel, Dordrecht (1983).Google Scholar
  13. 13.
    D. Gabbay: Theoretical foundations for non monotonic reasoning in expert systems. RR 84 Imperial college (1984).Google Scholar
  14. 14.
    S. Kripke: Semantical considerations on modal logic. In L.Linsky (eds.): Reference and modality. Oxford Univ Press, LONDON pp. 63–72 (1971).Google Scholar
  15. 15.
    J.L. Laurière: Un langage déclaratif:SNARK. TSI 3 pp. 141–170(1896).Google Scholar
  16. 16.
    LEA SOMBE: Inférences non classiques en I.A. 2∘ journées Proc GRECO I.A pp. 137–230 (1988).Google Scholar
  17. 17.
    R.C. Moore: Autoepistemic logic in P.Smets(eds): Non standard logics for automated reasoning. Acad press London pp. 105–136 (1988).Google Scholar
  18. 18.
    R.C. Moore: Semantical considerations on non monotonic logic. A.I. 25(1) pp. 75–94 (1985).Google Scholar
  19. 19.
    D. Miller: A logical analysis of modules in logic programing. JLP. 7 pp. 79–108 (1989).Google Scholar
  20. 20.
    D. Pastre: MUSCADET: An automatic theorem proving using knowledge and metaknowledge in mathematics. A.I. 38(3) pp. 257–319 (1989).Google Scholar
  21. 21.
    R. Reiter: A logic for default reasoning. A.I. 13(1–2), pp. 81–131 (1980).Google Scholar

Copyright information

© Springer-Verlag 1993

Authors and Affiliations

  • D. Ferney
    • 1
  • A. Quilliot
    • 1
  1. 1.Université Blaise PascalAubiereFrance

Personalised recommendations