From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2348 Path: news.gmane.org!not-for-mail From: "Jean-Pierre Marquis" Newsgroups: gmane.science.mathematics.categories Subject: RE: Semantic tableaux and intuitionistic logic Date: Mon, 9 Jun 2003 10:05:01 -0400 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018596 3709 80.91.229.2 (29 Apr 2009 15:23:16 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:23:16 +0000 (UTC) To: Original-X-From: rrosebru@mta.ca Mon Jun 9 11:52:10 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:52:10 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNyz-0003bC-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:50:49 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 39 Original-Lines: 47 Xref: news.gmane.org gmane.science.mathematics.categories:2348 Archived-At: 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