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.
  • New routine "applyOnce": this routine is introduced to preceed a given rule call. In fact, when applying a given rule on a partial tableau, LoTREC looks for every graph pattern matching the rule's conditions set and apply the rule's actions set on ALL THE MATCHING PATTERNS. That's why the user cannot apply a rule in ONLY ONE matching pattern, then memorize that it's done, in order to not apply on other matching patterns. For example, when two <U> phi are found in two diffrent nodes at the same time, the rule creating <U> successors will create TWO successors and cannot test if it was applied somewhere until the NEXT iteration of the strategy.
  • Model editor (prototype): LoTREC tableaux builder is equipped with a tableaux editor, to manually (without respect to the given tableau rules) prepare a pre-model or to change a candidate model during its construction. This is very useful with Step-by-Step run mode, to help testing huge formulas or reduce the calculus time cost, and then to focus on a partial result when it's needed.
  • Graphical User Interface for logic definition: a user freindly GUI to enable add/edit or delete any part of a logic definition. This makes defining new logics much easier and error free.
  • XML standalone files: a LoTREClogic definition is hold in xml files, containing the set of rules and strategies used for the logic and an eventual set of testing formulas. Every part in the file could be commented to make logic files exchange between the researchers in the domain easier and clearer.


Online Users' Manual: it's a shared task for our research team memebers. We hope have a basic version at the begining of May 2008. The tutorials and other help documentations will come soon later when the GUI becomes more stable.

Copy/Paste and Auto-completion facilities for rules definitions, more precisely for conditions and actions. For the moment, we will try to offer a predefined set of rules, than to import from other logic files and finally, we hope accomplish the two mentioned new features.

In-line model editing: thus the user can change his tableaux graphically in place. The current version is working well, but through text fields in a seperate dialog box.

Graph Visiualization Toolkit replacement: for the moment, we are using Cytoscape (an "application" of completely diffrent purpose) to help us display and layout our tableaux. This choice was made at an earlier stage of LoTREC current version developpement. For many reasons, especially memory management and performance issues, we are looking forward to replace Cytoscape by Prefuse (a "tollkit" which is more likely what we are looking for).

(1), (2) requires Java Runtime Environement (JRE) 6 (or later)