Optimization of deduction for Multi-Modal Logics

  • Olivier Gasquet
Part of the Synthese Library book series (SYLI, volume 247)


Automated deduction methods facilitate the usage of modal logic in AI. Beside methods, both based on deduction rules for the object language (Fitting, 1983) (Enjalbert Fariñas del Cerro, 1986), there are translation methods that rely on an embedding of the Kripke semantics into first-order logic. Translation methods may carry an advantage in that they are modular, and offer the possibility to re-use the tools, strategies, provers... that have been designed and used for classical logic for about 30 years. Translation methods can be divided into two distinct approaches:
  • The relational translation (Moore, 1980): the target logic contains one or more distinguished predicate(s) that simulate the relation(s) in the Kripke semantics. Thus the formula ǹp is translated into (∃W0∀w)(R(w0, w)→ p(w)) where w0 is the initial world and p(w) denotes in the target language that p (propositional variable of the object language) is true at the world w. Of course, this translation preserves satisfiability, and if the relations satisfy some property, reflexivity for example, this must be reflected by a theory in the target logic. As one can see, this translation is a direct simulation of the Kripke semantics. In the predicate case, a modal formula such as ǹp(x) is translated into (∃W0∀w)(R(w0, w)→ p(x, w)). With this method, it is necessary to provide a special treatment for the R-predicate(s). (Frisch Scherl, 1991)).


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Peter B. Andrews, “An introduction to mathematical logic and type theory: to truth though proof”, Academic Press, 1986.Google Scholar
  2. Yves Auffray & Patrice Enjalbert, “Modal theorem proving: An equational view point”, Int. Joint Conf. on AI, 1989.Google Scholar
  3. Laurent Catach, “Normal multimodal logics”, Proc. Nat. Conf. on AI (AAAIJ88), p. 491–495, 1988.Google Scholar
  4. Laurent Catach, “Les logiques multimodales”, Ph. D. thesis, Universite Paris VI, France, 1989.Google Scholar
  5. F. Debart, P. Enjalbert & M. Lescot, “Multi-modal deduction using Equational and Order-Sorted Logic”, Proc. 2nd Conf. on Conditional Rewriting Systems, to appear in Springer LNCS, M. Okada & S. Kaplan ed., Montreal, 1990.Google Scholar
  6. P. Enjalbert, Luis Farinas del Cerro, “Modal Resolution in Clausal Form”, Theoretical Computer Science, Vol. 65, pp. 1–33, 1986.CrossRefGoogle Scholar
  7. Luis Farinas del Cerro & Andreas Herzig, “Deterministic Modal “Deterministic Modal Logic for Automated Deduction”, 9th European Conference on Artificial Intelligence, Stockholm, 1990.Google Scholar
  8. Luis Fariñas del Cerro, Martti Penttonen, “Grammar Logics”, Synth se et analyse, vol. 121–122, pp. 123–134, 1988.Google Scholar
  9. Melvin Fitting, “Proof Methods for Modal and Intuitionistic Logics”, Synthese Library, Reidel, 1983.Google Scholar
  10. A. M. Frisch, R. Scherl, “A general framework for modal deduction”, 2nd Int. Conf. on Knowledge Representation and Reasoning, Allen, Fikes, et Sandewall (eds), Morgan Kaufmann, 1991.Google Scholar
  11. Olivier Gasquet, “A Unification Algorithm for Multimodal Logics with Persistence Axiom”, 5th International Workshop on Unification (UNIF’92), Barbizon, France, 1991.Google Scholar
  12. Olivier Gasquet, “Deduction automatique en logique multimodale par traduction”, Ph.D. thesis, Universite Paul Sabatier, Toulouse, France, 1994Google Scholar
  13. Olivier Gasquet, “Deduction for multi-modal logics”, Technical Report, IRIT, Toulouse, France, 1994.Google Scholar
  14. Andreas Herzig, “Raisonnement automatique en logique modale et algorithme d’unification”, Ph. D. thesis, Universite Paul Sabatier, Toulouse, France, 1989.Google Scholar
  15. Saul Kripke, “Semantical Analysis of Modal Logic I, Normal Propositional Calculi”, Zeitschrift für mathematische Logik und Grunlagen der Mathematik, 9, 1963.Google Scholar
  16. R.C. Moore, “Reasoning about Knowledge and Action”, Ph. D. Thesis, MIT, Cambridge, Massachussets, 1980.Google Scholar
  17. Hans Jürgen Ohlbach, “A Resolution Calculus for Modal Logics”, Proceedings of 9th CADE, LNCS 310, Springer Verlag, 1988.Google Scholar
  18. Hans Jürgen Ohlbach, “Semantics-Based Translation Method for Modal Logics”, In: Journal of Logic and Computation, Dov Gabbay editor, Vol. 1, 5, pp. 691–746, 1991.CrossRefGoogle Scholar
  19. M. Schmidt-Schauß, “Computational Aspects of an Order-Sorted Logic with Term Declarations”, in Lecture Notes in Artificial Intelligence, J. Siekmann editor, Vol. 395, Springer-Verlag, 1989.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 1995

Authors and Affiliations

  • Olivier Gasquet
    • 1
  1. 1.Institut de Recherche en Informatique de Toulouse (IRIT)ToulouseFrance

Personalised recommendations