A proof-search procedure for intuitionistic propositional logic

Archive for Mathematical Logic 52 (7-8):759-778 (2013)
  Copy   BIBTEX

Abstract

A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.

Categories

Keywords

Reprint years

DOI

10.1007/s00153-013-0342-y

Links

PhilArchive



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

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

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.
Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
On second order intuitionistic propositional logic without a universal quantifier.Konrad Zdanowski - 2009 - Journal of Symbolic Logic 74 (1):157-167.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
Glivenko type theorems for intuitionistic modal logics.Guram Bezhanishvili - 2001 - Studia Logica 67 (1):89-109.
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.Linda Postniece - unknown
Propositional Mixed Logic: Its Syntax and Semantics.Karim Nour & Abir Nour - 2003 - Journal of Applied Non-Classical Logics 13 (3-4):377-390.
A short proof of Glivenko theorems for intermediate predicate logics.Christian Espíndola - 2013 - Archive for Mathematical Logic 52 (7-8):823-826.
On different intuitionistic calculi and embeddings from int to S.Uwe Egly - 2001 - Studia Logica 69 (2):249-277.
New sequent calculi for Visser's Formal Propositional Logic.Katsumasa Ishii - 2003 - Mathematical Logic Quarterly 49 (5):525.
Glivenko Theorems for Substructural Logics over FL.Nikolaos Galatos & Hiroakira Ono - 2006 - Journal of Symbolic Logic 71 (4):1353 - 1384.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
On the linear decoration of intuitionistic derivations.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - Archive for Mathematical Logic 33 (6):387-412.

Analytics

Added to PP
2013-12-01

Downloads
42 (#361,008)

6 months
4 (#698,851)

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

Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.

Add more references