Are there any proof assistants or theorem provers based on the method of analytic tableaux?
A closed tableau makes the branching structure of a proof using case analysis very obvious.
I like tableau calculi for proving stuff by hand; especially validating simple statements in nonclassical propositional or modal logics. For this purpose, tableau calculi are quite convenient and tableau proofs are short.
For larger things though, especially when using FOL, proving something by hand using this method is tedious ... largely because of the need to Skolemize the formula and rewrite the matrix of wffs in negation normal form.
I'm curious whether there are any well-known proof assistants based on the method of analytic tableaux or are capable of exporting tableau proofs in some format.