A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications

, &
Journal of Applied Non-Classical Logics 19 (2):149-166 (2009)
  Copy   BIBTEX

Abstract

Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and the width of proofs with respect to Hudelmaier's one. These improvements have a significant influence on the performances of the implementation.

Categories

Keywords

Reprint years

DOI

10.3166/jancl.19.149-166

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 99,484

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic.P. Miglioli, U. Moscato & M. Ornaghi - 1997 - Logic Journal of the IGPL 5 (1):145-167.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
A secondary semantics for Second Order Intuitionistic Propositional Logic.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2004 - Mathematical Logic Quarterly 50 (2):202-210.
On the computational content of intuitionistic propositional proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
Cut-free tableau calculi for some intuitionistic modal logics.Mauro Ferrari - 1997 - Studia Logica 59 (3):303-330.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Intuitionistic Socratic procedures.Tomasz F. Skura - 2005 - Journal of Applied Non-Classical Logics 15 (4):453-464.
Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculi.Evgeny Zolin - 2014 - Studia Logica 102 (5):1021-1039.
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems.Tim Lyon - 2013 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734). Springer. pp. 177-194.
A tableau calculus with automaton-labelled formulae for regular grammar logics.Rajeev Gore - unknown

Analytics

Added to PP
2013-12-25

Downloads
312 (#80,405)

6 months
4 (#1,151,070)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Modal logic.Alexander Chagrov - 1997 - New York: Oxford University Press. Edited by Michael Zakharyaschev.
Investigations into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
Intuitionistic logic, model theory and forcing.Melvin Fitting - 1969 - Amsterdam,: North-Holland Pub. Co..
Investigations into Logical Deduction.Gerhard Gentzen, M. E. Szabo & Paul Bernays - 1970 - Journal of Symbolic Logic 35 (1):144-145.
Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.

View all 7 references / Add more references