I'm currently doing research on computational discourse semantics and I

wonder if anybody has a theorem prover, written in Prolog, to share with

me. It should (of course) be for a logic more expressive than horn

clause logic, and as I want to be able to follow the structure of the

proofs, preferably a non-resolution method should be used (a tableaux

method, for example). Programs and/or advices and/or pointers to

relevant literature are most welcome.

Thanks for your help.

Department of Philosopy

S-412 98 Gothenburg

Sweden