Talking About Graphs
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.
KeywordsModel Check Modal Logic Inference Rule Propositional Logic Atomic Formula
- [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
- [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