Lotrecscheme : graphical generic tool for tableau methods

(then extract and launch 'java -jar dist/lotrecscheme.jar')
Write graphically tableau methods for normal modal logics.
Customize your tableau methods with Scheme code.
Debug tableau methods
Read the manual

Download also tableau method for K, KT, S4, S4.3, S5, S5_n, S5_n-PAL, etc.

You can then execute your tableau method step-by-step.

Finally you can get a model for your formula if it is satisfiable.