Tableaux 2009 - Tutorial

LoTREC: Theory and Practice.

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.

One main feature of LoTREC is to offer a high-level language for describing rewrite rules over a graph, and a very simple language for describing what we call a strategy, i.e. a description of the rules application order. This allows LoTREC to be used for one’s own logic by non-computer scientists since only small programming skills are necessary.
Another good reason for choosing LoTREC is that it is accessible via the web with one click installation. It has a rich graphical user interface that makes it easy to define new tableau calculi and to visualize the graph models.
Currently in LoTREC, we have tableau provers for various propositional logics such as CPL, K, KT, S4, KD45, S5, K + Confluence, K + the universal modality, LTL, PDL and many others...

In this tutorial, we give an overview of the theoretical basis of LoTREC, and then we give a demonstration on how to use LoTREC to build tableau provers for various propositional non-classical logics with a bunch of examples. This tutorial requires a basic knowledge of tableau calculi for propositional standard modal logics and some of its basic techniques such as loop-check.