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:

LoTREC output is all the models and/or counter-models for the input formula in form of tableaux trees.