LoTREC: possible worlds finally made accessible

NEW: Kripke's Worlds published

Learning by doing, on a subject usually perceived as rather abstract: modal logics...

NEW: LoTREC 2.0.1 (Beta version)

NEW: Video Tutorials

Three video tutorials are available to start with LoTREC:...


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.

Kripke's World

Kripke's World

This tutorial is one of the events of the 3rd World Congress and School on Universal Logic 2010.


S4 with histories

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:

LoTREC 2.0 Release

What's New

  • Tableau builder controls: stop, pause/resume mode were introduced to give the user more control during the tableaux construction. Thus, endless loops, that may be raised from unpredicted behavior of some rules combinations, can be stopped manually by the user.
  • Step-by-Step run mode: users can make break points on any sub set of their rules, such that LoTREC will show how the models built change when applying a given tableau rule.

K + Universal Modalities

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.

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.

Syndicate content