Here you can prove formulas with the semantic tableau method. The derivation rules are defined in ATL.

You can choose to use the Sandbox, where everybody can add and edit and remove derivation rules, or you can start a new project where you need a password to modify rules.
The list of projects is here.

A little more help for new users is available here.