A tableau calculus for propositional intuitionistic logic with a refined treatment of nested implications


Since 1993, when Hudelmaier developed an O-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 F c with a new set of rules to treat signed formulas of the kind T → 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.

Download options


    Upload a copy of this work     Papers currently archived: 72,805

External links

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

Through your library


Added to PP

298 (#37,042)

6 months
1 (#386,499)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Modal Logic.Alexander Chagrov - 1997 - Oxford, England: Oxford University Press.
Investigations Into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
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

Citations of this work

No citations found.

Add more citations

Similar books and articles

A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
Quantum Logical Calculi and Lattice Structures.E. -W. Stachow - 1978 - Journal of Philosophical Logic 7 (1):347 - 386.
The Logic of Bunched Implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Cut Elimination for Propositional Dynamic Logic Without.Robert A. Bull - 1992 - Mathematical Logic Quarterly 38 (1):85-100.