Hi everyone, I'd just like to announce the first release of Tableaux, a web-based interactive theorem prover for first-order logic based on the method of semantic tableaux (cf. "First-Order Logic", Raymond Smullyan, Dover). This prover was intended as a teaching aid for undergraduate students and enforces a step-by-step construction of proofs. It could also be used as a basis for provers for other logics. Tableaux runs on any web server supporting the CGI interface; uou can check it out at http://www.ncc.up.pt/~pbv/cgi/tableaux.cgi. The source package is available from Hackage: http://hackage.haskell.org/package/tableaux. Best regards, Pedro Vasconcelos