Nerode, Shore: logic for Applications, Springer, has detailed tableau development for intuitionistic, and modal logics: i.e. there is nothing intrinsically classical about the method. The ideas go back to Hintikka and Beth (at least) in the 1950s and 60s. On Fri, 30 May 2003, Galchin Vasili wrote:
Hello,
I am only familiar with semantic tableaux for classical propositional logic (and classical 1st order logic). It seems that as an inference system it is based squarely around the law of the excluded middle because it is essentially reductio ad absurdum. Hence, as an inference system it can't be simply modified for intuitionistic propositional calculus?? (Of course, I am bringing this because the role that Heyting algebras play in Topos theory).
Regards, Bill Halchin
-------------------------------------------------------------------- Jim Lipton Math Dept.Wesleyan University, Middletown,CT 06459-0128 www.wesleyan.edu/~jlipton jlipton@wesleyan.edu, (860) 685-2188 fax:685-2571 ====================================================================