Molle is a cross-platform prover for modal logic, that exploits
the modal semantic tableaux method.
It features a very usable graphical interface, with interactive
representation of generated models.
Molle is maintained by Dipartimento di Elettronica e
Informazione, at Politecnico di Milano.