The last years have seen a renewed interest in modal and description logics (MDLs). Better algorithms, coding, and technology
have led to effective systems based on tableau and constraint systems [6
7] to DPLL-based implementations
Behind Lotrec is the work on modal tableaux with back/forth rules [9], graphs [1,2], and its DL counterpart in [7]. Lotrec has been implemented by D. Fauthoux [4]
Acknowledgements Thanks to the LILaC members who tested Lotrec and helped to improve it by their comments, in particular L. Aszalos, J.-F.
Condottta, Th. Polacsek, and S. Suwanmanee. F. Massacci acknowledges the CNR Fellowship CNR-203-07-27.