LoTREC User's Manual
...
Overview
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.
LoTREC takes as input three parameters:
- Logic definition: (generally) an XML file describing the set of connectors used in the formulas, the set of tableau rules and strategies for applying them in a suitable order
- Strategy: chosen among the ones defined in the logic file
- Formula: to be tested
LoTREC output is all the models and/or counter-models for the input formula in form of tableaux trees.
Logic Definition
Formulas
The user can use any word, starting with a capital letter, as an atomic proposition. Formulas are then defined recursively using a set of connectors defined by the user.
Connectors
A connector is tuple (name, arity, output-format, priority).
name: is the identifier of the connector. It can be used in the prefixed formulas definition.
arity: determins the number of arguments it takes in this connector.
output-format: is the infixed definition of the connector.
priority: is used to precise prioirties between connectors when ambiguity may rise in infixed formulas.
Rules
Strategies
Run Settings
Build Tableaux
Tableaux Tree sample
Tableau sample for []~[]P in S4
Auto-Layouting sample