Molle is the Modal Logic Loony Evaluator.
Molle is a cross-platform prover written in Java™ that implements the tableaux algorithm for the K modal logic. It can prove the validity of modal fomulae and generate example and counterexample models.
Frame properties can be selected: the reflexive property has been implemented so far, and more properties will be in the short term. The goal is to have all the major modal logics available for proving.
Molle features a very usable graphical interface and a simple syntax for formulae. With next to no learning curve, Molle is extremely well suited for teaching and practicing with modal logics.
Mollicino is the Java Web Start release of Molle. It is equivalent to Molle, but it can be started by any web browser, at any location, without the need to download a package manually.