In this course I will develop systematically and illustrate with many examples the incremental tableau-building methodology for constructive testing of satisfiability, applicable to a wide variety of logical systems. I will focus first on linear and branching time temporal logics, and then on multi-agent logics of (individual, common, and distributed) knowledge, time, and strategic abilities (of the type of the alternating-time temporal logic ATL). Also, I will discuss how the tableau methodology can be applied to model-checking in these logics. I will sketch proofs of termination, soundness, and completeness of the tableau methods, will discuss their complexity, and will discuss how satisfying models can be extracted from open tableaux.
The two main objectives of the course will be to give the students practical skills of applying the methods presented in the course, and the theoretical understanding of the tableau-building methodology that would enable them to construct similar decision methods for other logics of their interest.
