The following references might be of some interest: Bell, J.L. & DeVidi, D., Solomon, G., 2001, Logical Options, Broadview Press. Marcello D'Agostino, Dov M. Gabbay, Reiner Hahnle, Joachim Posegga, 1999, Handbook of Tableau Methods, Kluwer Academic Pub. Jean-Pierre Marquis -----Message d'origine----- De : cat-dist@mta.ca [mailto:cat-dist@mta.ca]De la part de Thomas Streicher Envoye : 6 juin, 2003 04:14 A : categories@mta.ca Objet : categories: Re: Semantic tableaux and intuitionistic logic
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).
the point is that tableau calculus may be best understood as a search for cut-free proofs in either classical or intuitionistic logic; this fact is systematically overlooked in the literature on tableaux methods like in the logic programming community one hardly ever finds exposed the view that executing a logic program is nothing but unravelling an inductive definition for information on tableau methods from a proof-theoretic point of view see Troelstra & van Dalen's book "Constructivism in Mathematics" vol.2, the chapter on proof theory of intuitionistic logic Best, Thomas