NEW: Video Tutorials
Tue, 02/12/2013 - 12:37 — Olivier Gasquet- Launch LoTREC from scratch : Launching LoTREC
- Test an implemented modal logic: Quick start (beginners)
- Implement a modal logic from scratch: Quick start (advanced)
LoTREC 2.0 Release
Mon, 04/14/2008 - 15:16 — Bilal SaidLoTREC 2.0 is released:
- Launch the LoTREC Web Start (1)
- Download executable package (2)
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 SaidLoTREC 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
Fri, 04/16/2010 - 10:53 — Andreas HerzigKripke's World
This tutorial is one of the events of the 3rd World Congress and School on Universal Logic 2010.
Description:
S4 with histories
Wed, 02/04/2009 - 20:06 — Bilal SaidSince 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 SaidA 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
Thu, 04/03/2008 - 15:16 — Bilal SaidLoTREC: Theory and Practice.
Proving by Tableau becomes easier...
This tutorial is 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.
