LoTREC 2.0 Release

Mon, 04/14/2008 - 15:16 — Bilal Said

LoTREC 2.0 is released:

Launch the LoTREC Web Start ⁽¹⁾

Download executable package ⁽²⁾

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.

Overview

Thu, 04/03/2008 - 17:09 — Bilal Said

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.

S4 with histories

Wed, 02/04/2009 - 20:06 — Bilal Said

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:

K + Universal Modalities

Mon, 04/14/2008 - 12:54 — Bilal Said

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.

Tutorials

Thu, 04/03/2008 - 15:16 — Bilal Said

LoTREC: Theory and Practice.

Proving by Tableau becomes easier...

This tutorial was one of the events of Tableaux 2009.

Description:

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.