The Basics of the Model Construction Method

  • Olivier Gasquet
  • Andreas Herzig
  • Bilal Said
  • François Schwarzentruber
Part of the Studies in Universal Logic book series (SUL)


This chapter is about the basic modal logic K and its multimodal version K n . We also present the basic description logic ALC, which can be viewed as a notational variant of K n . The implementation of reasoning methods for all these logics can be done by means of the most basic rules, that are combined by the most basic strategies: fair strategies.


Prefix Tame 
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. [BBW06]
    P. Blackburn, J.F.A.K. van Benthem, and F. Wolter. Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning. Elsevier Science, New York, 2006. Google Scholar
  2. [BdRV01]
    P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2001. MATHGoogle Scholar
  3. [Bet55]
    E.W. Beth. Semantic entailment and formal derivability. In Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, N.R, volume 18(3), pages 309–342, 1955. Reprinted in Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969. Google Scholar
  4. [BS00]
    F. Baader and U. Sattler. Tableau algorithms for description logics. Studia Logica, 69:2001, 2000. MathSciNetGoogle Scholar
  5. [CZ97]
    A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford Logic Guides. Oxford University Press, London, 1997. MATHGoogle Scholar
  6. [Fit83]
    M. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel, Dordrecht, 1983. CrossRefMATHGoogle Scholar
  7. [GKWZ03]
    D.M. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam, 2003. Google Scholar
  8. [Gor99]
    R. Goré. Tableau methods for modal and temporal logics. In M. D’Agostino, D.M. Gabbay, R. Hähnle, and J. Posegga, editors, Handbook of Tableau Methods, pages 297–396. Hingham, MA, USA. Kluwer Academic, Dordrecht, 1999. CrossRefGoogle Scholar
  9. [Hor98a]
    I. Horrocks. The fact system. In H. de Swart, editor, Proc. of the 2nd Int. Conf. on Analytic Tableaux and Related Methods (TABLEAUX’98), volume 1397 of Lecture Notes in Artificial Intelligence, pages 307–312. Springer, Berlin, 1998. CrossRefGoogle Scholar
  10. [Hor98b]
    I. Horrocks. Using an expressive description logic: FaCT or fiction. In Proc. of the 6th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’98), pages 636–647, 1998. Google Scholar
  11. [NPW02]
    T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL—A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, Berlin, 2002. MATHGoogle Scholar
  12. [Pau89]
    L.C. Paulson. The foundation of a generic theorem prover, Journal of Automated Reasoning, 5, 1989. Google Scholar
  13. [Smu95]
    R. Smullyan. First Order-Logic. Dover, New York, 1995. First print: 1968. Google Scholar
  14. [TH06]
    D. Tsarkov and I. Horrocks. Fact++ description logic reasoner: system description. In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006), volume 4130 of Lecture Notes in Artificial Intelligence, pages 292–297. Springer, Berlin, 2006. CrossRefGoogle Scholar

Copyright information

© Springer Basel AG 2014

Authors and Affiliations

  • Olivier Gasquet
    • 1
  • Andreas Herzig
    • 1
  • Bilal Said
    • 1
  • François Schwarzentruber
    • 1
  1. 1.Institut de Recherche en Informatique de Toulouse (IRIT)Université Paul SabatierToulouseFrance

Personalised recommendations