Translating inaccessible worlds logic into bimodal logic

  • Olivier Gasquet
  • Andreas Herzig
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 747)


This paper addresses the problem of automated deduction for Humberstone's inaccessible worlds logic. We exhibit a sound and complete translation into a normal bimodal logic for which efficient proof methods have been devised in the last years. By the way, our translation provides a sound, complete and finitary axiomatization of Humberstone's inaccessible worlds logic.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. L. Catach, “Normal multimodal logics”. Proc. Nat. Conf. on AI (AAAI 88), pp. 491–495, 1988.Google Scholar
  2. Luis Fariñas del Cerro, Andreas Herzig, “Automated Deduction for Epistemic and Temporal Logics”. Handbook of Logic in AI (eds D. Gabbay, A. Galton, C. Hogger), Oxford University Press, to appear.Google Scholar
  3. Olivier Gasquet, “Deduction for Multimodal Logics”. International Conference on Applied Logic (Logic at Work'93), Amsterdam, Holland, 1993.Google Scholar
  4. Valentin Goranko, “Modal Definability in Enriched Languages”. Notre Dame Journal of Formal Logic, vol. 31, 81–105, 1990.Google Scholar
  5. Valentin Goranko, Solomon Passy, “Using the Universal Modality: Profits and Questions”. Report, Sofia University, July 1989.Google Scholar
  6. G. Hughes, M. J. Cresswell, “A companion to modal logic”. Methuen & Co. Ltd, 1984.Google Scholar
  7. I. Humberstone, “Inaccessible worlds”. Notre Dame Journal of Formal Logic, vol. 24, 346–352, 1983.Google Scholar
  8. H. Levesque, “All I know: A study in autoepistemic logic”. J. of AI, 42: 263–309, 1990.Google Scholar
  9. Andreas Nonnengart, “First-Order Modal Logic Theorem Proving and Functional Simulation”, International Joint Conference on Artificial Intelligence, Chambéry, France, 1993.Google Scholar
  10. Hans Jürgen Ohlbach, “Semantics-Based Translation Method for Modal Logics”. J. of Logic and Computation, Vol. 1, 5, pp. 691–746, 1991.Google Scholar
  11. Hans Jürgen Ohlbach, “Optimized Translation of Multi-Modal Logic into Predicate Logic”. Proc. of Logic Programming and Automated Reasoning (LPAR), (ed. A. Voronkov), Springer Verlag, LNAI, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Olivier Gasquet
    • 1
  • Andreas Herzig
    • 1
  1. 1.IRITUniversité Paul SabatierToulouse CedexFrance

Personalised recommendations