Another possibility is MleanCoP: http://www.leancop.de/mleancop/ I also think Isabelle is worth the effort. It's been adapted to modal logic, for philosophical purposes, by Christoph Benzmuller et al. - you can find links to their work here: http://page.mi.fu-berlin.de/cbenzmueller/compmeta/htdocs/