Graduate studies at Western
|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)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
Matthias Baaz & Rosalie Iemhoff (2006). Gentzen Calculi for the Existence Predicate. Studia Logica 82 (1):7 - 23.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Roy Dyckhoff & Sara Negri (2000). Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. Journal of Symbolic Logic 65 (4):1499-1518.
A. Carbone (2002). The Cost of a Cycle is a Square. Journal of Symbolic Logic 67 (1):35-60.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Added to index2009-01-28
Total downloads10 ( #114,394 of 729,984 )
Recent downloads (6 months)1 ( #61,087 of 729,984 )
How can I increase my downloads?