30 May
2003
30 May
'03
8:14 p.m.
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