Hello, Here is an intuitionistic logic theorem prover that might be interesting in light of the relationship of Heyting algebras to topoi: http://www.intellektik.informatik.tu-darmstadt.de/~jeotten/ileanTAP/ Regards, Bill Halchin