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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,122

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

A secondary semantics for Second Order Intuitionistic Propositional Logic.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2004 - Mathematical Logic Quarterly 50 (2):202-210.
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.
A Finite Hilbert‐Style Axiomatization of the Implication‐Less Fragment of the Intuitionistic Propositional Calculus.Jordi Rebagliato & Ventura Verdú - 1994 - Mathematical Logic Quarterly 40 (1):61-68.
On the period of sequences (an(p)) in intuitionistic propositional calculus.Wim Ruitenburg - 1984 - Journal of Symbolic Logic 49 (3):892 - 899.
A tableau calculus with automaton-labelled formulae for regular grammar logics.Rajeev Gore - unknown
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
A modal calculus analogous to k4w, based on intuitionistic propositional logic, iℴ.Aldo Ursini - 1979 - Studia Logica 38 (3):297 - 311.
Quantum logical calculi and lattice structures.E. -W. Stachow - 1978 - Journal of Philosophical Logic 7 (1):347 - 386.
Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculi.Evgeny Zolin - 2014 - Studia Logica 102 (5):1021-1039.
A sound and complete tableau calculus for reasoning about only knowing and knowing at most.Riccardo Rosati - 2001 - Studia Logica 69 (1):171-191.
The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Cut-free tableau calculi for some intuitionistic modal logics.Mauro Ferrari - 1997 - Studia Logica 59 (3):303-330.
The Decidability of Dependency in Intuitionistic Propositional Logi.Dick De Jongh & L. A. Chagrova - 1995 - Journal of Symbolic Logic 60 (2):498 - 504.
Cut elimination for propositional dynamic logic without.Robert A. Bull - 1992 - Mathematical Logic Quarterly 38 (1):85-100.

Analytics

Added to PP
2013-12-25

Downloads
300 (#63,857)

6 months
2 (#1,015,942)

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.
Modal Logic.Yde Venema, Alexander Chagrov & Michael Zakharyaschev - 2000 - Philosophical Review 109 (2):286.
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.

View all 8 references / Add more references