Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents

In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 43-66 (2008)

Abstract
We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
ISBN(s)
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,385
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Constructive Negation, Implication, and Co-Implication.Heinrich Wansing - 2008 - Journal of Applied Non-Classical Logics 18 (2-3):341-364.
Display Logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.
Cut-Free Sequent Calculi for Some Tense Logics.Ryo Kashima - 1994 - Studia Logica 53 (1):119 - 135.

View all 10 references / Add more references

Citations of this work BETA

Constructive Negation, Implication, and Co-Implication.Heinrich Wansing - 2008 - Journal of Applied Non-Classical Logics 18 (2-3):341-364.
Natural Deduction for Bi-Intuitionistic Logic.Luca Tranchini - 2017 - Journal of Applied Logic 25:S72-S96.

Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total views
40 ( #228,363 of 2,291,314 )

Recent downloads (6 months)
1 ( #827,672 of 2,291,314 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature