Advertisement

Talking About Graphs

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

Abstract

We introduce a general formal language in order to talk about properties of Kripke models. We then show how such languages can be defined in LoTREC and how to check that a formula is true in a given world of a given Kripke model. The latter is called model checking. Beyond model checking we also introduce the reasoning tasks of satisfiability checking, validity checking, and model building. We show that all other tasks can be reduced to the latter, which we focus on in the rest of the book: we show how to build models for a series of logics. These logics are grouped into families, according to the techniques the tableaux implementation in LoTREC requires.

Keywords

Prefix 
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.

References

  1. [AtC06]
    C. Areces and B. ten Cate. Hybrid logics. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3. Elsevier Science, Amsterdam, 2006. Google Scholar
  2. [AvBN98]
    H. Andréka, J.F.A.K. van Benthem, and I. Nemeti. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217–274, 1998. MathSciNetCrossRefMATHGoogle Scholar
  3. [BK08]
    C. Baier and J.-P. Katoen. Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge, 2008. MATHGoogle Scholar
  4. [Coo71]
    S.A. Cook. The complexity of theorem proving procedures. In Proceedings Third Annual ACM Symposium on Theory of Computing, pages 151–158. ACM, New York, 1971. CrossRefGoogle Scholar
  5. [Kle67]
    S.C. Kleene. Mathematical Logic. Wiley, New York, 1967. MATHGoogle Scholar
  6. [Var96]
    M.Y. Vardi. Why is modal logic so robustly decidable. In N. Immerman and P.G. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 149–184. American Mathematical Society, Providence, 1996. Google 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