Yes, I know that Greg scooped me on this one, but Thomas Sutton has started a blog charting his development of a modal logic theorem prover written in Haskell and based around labelled tableaux. I point you to: Labelled Tableaux.
Labelled what you ask? A tableau is a proof theoretic gadget that looks and feels much like a collection of "uspide down sequent rules". The idea of tableaux is that instead of proving a formula, we show that its negation is inconsistent with the logic. This works especially well in the case of modal logic, since the tableau rules tend to match the frame semantics quite closely. Moreover, if the statement is not a theorem, then we can extract a countermodel from the failed proof search. This is quite dandy! For an introduction to tableau calculi for modal logic, including as much modal logic as is required, see:
Tableau Methods for Modal and Temporal Logic, Rajeev Gore'
(Full disclosure: Raj is one of my PhD supervisors. Of course, I give the article three thumbs up :)
So, what is all this labelling about then? Well, modal proof theory is a tricky thing to get right. In order to avoid nasty things such as infinite looping during proof search, many people have incorporated "labels" into their tableau calculi. This is not so nice from a theoretical point of view, since it obfuscates the essence of the logic and has a very "hacky" feel to it. Of course, if you are actually building a theorem prover, then labels are very handy!
A question that occurs to me is whether anyone has beaten semantic tableaux into providing systems for paraconsistent logics. This is a family of logics where an inconsitency does not necessarily trivialise the theory. Or, alternatively, where both a statement and its negation can be theorems! The basic strategy of attacking the negation of a formula seems, at first glance, to be at odds with this property. I'd be interested in any work that proves me otherwise.
Anyway, I'll be interested to see how the project turns out for Thomas. Maybe he'll let me play around with it when he is done... :)