Learning by doing, on a subject usually perceived as rather abstract: modal logics...
LoTREC is a generic tableau theorem prover for modal logic. It is a suitable educational tool for students and researchers for creating, testing and analysing tableau method implementations.
This tutorial is one of the events of the 3rd World Congress and School on Universal Logic 2010.
Since a naive tableau method for S4 may result in an endless loop (e.g. treating naively <>p), we usually add to our method some special techniques in order to guarantee its termination.
In an older version, we have implemented S4 in LoTREC using the loop-test technique. Such as done intuitively on paper, we avoided the endless loops by testing the inclusion of (the set of formulas of) new added nodes in (the set of formulas of) their ancestor nodes. Technically, this requires performing two complex tasks:
A new logic had been added to the library of predefined logics, and it will be integrated in the upcoming minor version release.
In this logic we use different techniques, such as history and model initialization, to optimize the tableau calculus. These techniques are ones of many others offered by LoTREC tableau engine and are needed when implementing an optimized tableau method for some logics such as S5 or PDL.
Proving by Tableau becomes easier...
This tutorial is one of the events of Tableaux 2009.
Unless they strictly use standard modal logics, people who work on the formalization of such and such concept are likely to be interested in the possibility of quickly implementing a prover or a model builder for their logics. LoTREC allows to handle almost any logic having a Kripke semantics, or more generally a semantics based in transition system, as long as a model builder for it can be expressed as a graph rewriting system, i.e. as long as we are able to express its semantical constraints with graph rewriting rules.