Advertisement

Resolution Modal Logics

  • Luis Fariñas-del-Cerro
Part of the NATO ASI Series book series (volume 13)

Abstract

In this paper we describe a general way to define a resolution method in the framework of non classical logics.

Keywords

Normal Form Modal Logic Inference Rule Classical Logic Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. [AR]
    ANDERSON, R., Improved decision procedures for Lewis’s calculus S4 and von Wright’s calculus. J.S.L., Vol. 19, 3, (1953), pp. 101–214.Google Scholar
  2. [BA]
    BAYART A., On truth-tables for M, B, S4 and S5. Logique et Analyse, Sept. 1970, pp. 335–375.Google Scholar
  3. [CR]
    CARNAP, R., Modalities and quantification. J.S.L., vol. 11, 2, (1946), pp. 33–64.MATHMathSciNetGoogle Scholar
  4. [CF1]
    CAVALLI, A.R., FARINAS DEL CERRO, L., Specification and verification of networks protocols using temporal logic. Proceedings of the Sixième Colloque International sur la programmation, Springer-Verlag, LNCS no 167, (1984).Google Scholar
  5. [CF2]
    CAVALLI, A.R., FARINAS DEL CERRO, L., Adecision method for linear temporal logic. Proceedings of the Seventh International Conference on Automata Deduction, Springer-Verlag, LNCS n° 170, (1984).Google Scholar
  6. [CHL]
    CHANG, C., LEE, R., Symbolical logic and mechanical theorem proving. Academic Press, New-York, (1973).Google Scholar
  7. [CM1]
    CIALDEA, M., Une méthode de résolution pour la logique intuitionniste propositionnelle. Rapport LSI, Université Paul Sabatier, Toulouse, (1983).Google Scholar
  8. [CM2]
    CIALDEA, M., Ph.d. Thesis Université Toulouse III, in preparation.Google Scholar
  9. [CL]
    COMBES, P., LEFORT, V., Gentiane: un outil de preuve de cohérence de formules en logique temporelle. Note technique, CNET IPAA ILLC.Google Scholar
  10. [FC1]
    FARINAS DEL CERRO, L., Déduction automatique et logique modale. Thèse d’Etat, Université de Paris V II, 1981.Google Scholar
  11. [FC2]
    FARINAS DEL CERRO, L., Prolegomena for programming in modal logic. 6th European Meeting on Cybernetics and Systems Research, Vienne, Avril 1982, North-Holland, (1982).Google Scholar
  12. [FC3]
    FARINAS DEL CERRO, L., Logique modale et processus communicants. Colloque AFCET “Les mathématiques de l’Informatique”, Paris, (1982).Google Scholar
  13. [FC4]
    FARINAS DEL CERRO, L., A simple deduction method for modal logic. Information Processing Letters, Vol. 14, n°2, (1982).Google Scholar
  14. [FC5]
    FARINAS DEL CERRO, L., A deduction method for modal logic. Europeaan IA Conference, 11–14 July 1982, Orsay.Google Scholar
  15. [FC6]
    FARINAS DEL CERRO, L., Les modalités de la correction totale. RAIRO Informatique Théorique, Vol. 16, n°4, (1982), pp. 349–363.MATHGoogle Scholar
  16. [FC7]
    FARINAS DEL CERRO, L., Temporal reasoning and termination of programs. Proceedings IJCAI 1983.Google Scholar
  17. [FC8]
    FARINAS DEL CERRO, L., Un principe de résolution en logique modale. RAIRO Informatique Théorique, Vol. 18, n° 2, (1984).Google Scholar
  18. [FL]
    FARINAS DEL CERRO, L., LAUTH, E., Raisonnement temporel: une méthode de déduction. Rapport LSI, Université Paul Sabatier, Toulouse, Novembre 1982.Google Scholar
  19. [FS]
    FARINAS DEL CERRO, L., SOULHI, S., Mutual belief logic for processing definite reference. Proceedings of International Workshop on Natural Language Understanding and Logic Programming, Rennes, 18–20 Septembre 1984, North-Holland.Google Scholar
  20. [GO]
    GALLION, O., Implémentation d’un démonstrateur de théorèmes. Rapport LSI, Université Paul Sabatier, Toulouse, Novembre 1981.Google Scholar
  21. [HJ]
    HENRY, J., Implémentation d’un démonstrateur pour des clauses d’Horn en logique modale. Rapport LSI, Université Paul Sabatier, en préparation.Google Scholar
  22. [KR]
    KOCHUT, E., RYCHLINK, P., Applications of modal logic in information systems, in Bolc, L., (ed.), Translating natural language into logical form, Springer, Symbolic Computation serie, to appear.Google Scholar
  23. [LE]
    LAUTH, E., Une méthode de résolution linéaire ordonnées pour la logique temporelle linéaire. Rapport LSI-ENSEEITH, Université Paul Sabatier, Toulouse, (1983).Google Scholar
  24. [LE]
    LEMMON, E., An introduction to modal logic. Amer. Philo. Generaly Monograph, (1977).MATHGoogle Scholar
  25. [SM]
    SHIMURA, M., Resolution in a new modal logic. Proceedings IJCAI 79, pp. 809–814.Google Scholar
  26. [OE]
    ORLOWSKA, E., Resolution systems and their applications I & II. Fundamenta Informaticae, Vol. III, n°2, (1980), pp. 235–267 & 333–362.Google Scholar
  27. [RJ]
    ROBINSON, J., A machine oriented logic based on the resolution principle. J. ACM, 12, (1965), pp. 23–41.CrossRefMATHGoogle Scholar
  28. [RP]
    RYCHLINK, P., The use of modal default reasoning in information system. To appears in The Int. Journal of Man-Machine Studies.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1985

Authors and Affiliations

  • Luis Fariñas-del-Cerro
    • 1
  1. 1.Langages et Systèmes InformatiquesUniversité Paul SabatierToulouse CedexFrance

Personalised recommendations