Proof Methods for MHL

  • Andrzej IndrzejczakEmail author
Part of the Trends in Logic book series (TREN, volume 30)


The final Chapter covers proof theory of hybrid logics. In contrast to the rest of the book, where ND performs a priviliged position, we have tried to present almost all deductive systems constructed so far for hybrid logics and describe their most interesting features. It follows from the author's conviction that on the field of investigation on proof methods for modal logics, the application of hybrid languages instead of standard modal languages may offer a real breakthrough, so careful analysis is vital


Modal Logic Inference Rule Proof System Horn Clause Sequent Calculus 
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.


  1. [165]
    Kracht, M. 1996. Power and weakness of the modal display calculus. In Proof theory of modal logic, ed. H. Wansing, 93–121. Dordrecht: Kluwer.Google Scholar
  2. [18]
    Baldoni, M. 1998. Normal multimodal logics: Automatic deduction and logic programming extension PhD thesis, Torino.Google Scholar
  3. [11]
    Areces, C., and J. Heguiabehere. HyLoRes: Direct resolution for hybrid logics. Available on Hybrid Logic Homepage.Google Scholar
  4. [32]
    Blackburn, P. 2000. Internalizing labelled deduction. Journal of Logic and Computation 10(1): 137–168.CrossRefGoogle Scholar
  5. [44]
    Bolander, T. and T. Braüner. 2007. Tableau-based decision procedures for hybrid logic. Journal of Logic and Computation 16: 737–763.CrossRefGoogle Scholar
  6. [55]
    Braüner, T. 2004. Natural deduction for hybrid logic. Journal of Logic and Computation 14(3): 329–353.CrossRefGoogle Scholar
  7. [99]
    Gabbay, D. 1996. LDS-labelled deductive systems. Oxford: Clarendon Press.Google Scholar
  8. [21]
    Basin, D., S. Matthews, and L. Vigano. 1997. Labelled propositional modal logics: Theory and practice. Journal of Logic and Computation 7(6): 685–717.CrossRefGoogle Scholar
  9. [36]
    Blackburn, P., and M. Marx. 2002. Tableaux for quantified hybrid logic. In Tableaux 2002, LNAI 2381, eds. U. Egly, and C. Fermuller, 38–52.Google Scholar
  10. [280]
    Wansing, H. 1998. Displaying modal logics. Dordrecht: Kluwer Academic Publishers.Google Scholar
  11. [277]
    Tzakova, M. 1999. Tableau calculi for hybrid logics. In Conference on Tableaux Calculi and Related Methods (TABLEAUX), Saratoga Springs, ed. N. Murray, 278–292. USA: LNAI 1617.Google Scholar
  12. [2]
    D’Agostino, M. 1999. Tableau methods for classical propositional logic. In Handbook of tableau methods, eds. M. D’Agostino et al., 45–123. Dordrecht: Kluwer Academic Publishers.Google Scholar
  13. [79]
    Demri, S., and R. Goré. 1999. Cut-free display calculi for nominal tense logics. In Tableaux 99, LNAI 1617, ed. N. Murray, 155–170. Berlin: Springer.Google Scholar
  14. [164]
    Konikowska, B. 1997. A logic for reasoning about relative similarity. Studia Logica 58(1): 185–226.CrossRefGoogle Scholar
  15. [237]
    Russo, A. 1995. Modal labelled deductive systems. Dept. of Computing, Imperial College, London, Technical Report 95(7).Google Scholar
  16. [251]
    Seligman, J. 2001. Internalization: The case of hybrid logics. Journal of Logic and Computation 11: 671–689.CrossRefGoogle Scholar
  17. [286]
    Vickers, S. 1988. Topology via logic. Cambridge: Cambridge University Press.Google Scholar
  18. [150]
    Indrzejczak, A. 2002. Resolution based natural deduction. Bulletin of the Section of Logic 31(3): 159–170.Google Scholar
  19. [45]
    Bolander, T. and P. Blackburn. 2007. Termination for hybrid tableaus. Journal of Logic and Computation 17(3): 517–554.CrossRefGoogle Scholar
  20. [12]
    Areces, C., D. Gorin. 2005. Ordered resolution with selection for h(@). In Proceedings of LPAR 2004, eds. F. Baader and A. Voronkov, 125–141, LNCS 3452.Google Scholar
  21. [148]
    Indrzejczak, A. 2002. Hybrid system for (not only) hybrid logic. Abstracts of AiML 2002: 137–156, Toulouse.Google Scholar
  22. [250]
    Seligman, J. 1997. The logic of correct description. In Advances in Intensional Logic, ed. M. de Rijke, 107–135. Dordrecht: Kluwer.Google Scholar
  23. [78]
    Demri, S. 1999. Sequent calculi for nominal tense logics: A step towards mechanization¿ In Tableaux 99, LNAI 1617, ed. N. Murray, 140–154. Berlin: Springer.Google Scholar
  24. [83]
    van Eijck, J. 2002. Constraint tableaux for hybrid logics. Amsterdam: Manuscript CWI.Google Scholar
  25. [40]
    Blackburn, P., and B. ten Cate. 2002. Beyond pure axioms: Node creating rules in hybrid tableaux. In Hybrid logics, eds. C. Areces et al., 21–35.Google Scholar
  26. [248]
    Seligman, J. 1991. A cut-free sequent calculus for elementary situated reasoning. Technical Report HCRC/RP-22 HCRC, Edinburgh.Google Scholar
  27. [10]
    Areces, C., H. DeNivelle, and M. DeRijke. 2001. Resolution in modal, description and hybrid logic. Journal of Logic and Computation 11: 717–736.CrossRefGoogle Scholar
  28. [194]
    Negri, S. 2005. Proof analysis in modal logic. Journal of Philosophical Logic 34: 507–544.CrossRefGoogle Scholar
  29. [249]
    Seligman, J. 1992. Situated consequence in elementary situation theory. Logic Group Preprint IULG-92–16, Indiana University.Google Scholar
  30. [281]
    Wansing, H. 2002. Sequent systems for modal logics. In Handbook of philosophical logic, eds. D. Gabbay, and F. Guenthner, vol IV, 89–133. Dordrecht: Reidel Publishing Company.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Dept. LogicUniversity of LódzLódzPoland

Personalised recommendations