Cut-elimination and proof-search for bi-intutionistic logic using nested sequents
Date
2008
Authors
Gore, Rajeev
Postniece (previously Buisman), Linda
Tiu, Alwen
Journal Title
Journal ISSN
Volume Title
Publisher
College Publications
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.
Description
Keywords
Keywords: Automated proofs; Bi-intuitionistic logic; Cut elimination; Proof search; Search strategies; Sequent calculus; Biomineralization; Calculations; Differentiation (calculus); Pathology; Semantics; Syntactics; Formal logic Bi-intuitionistic logic; Display calculi; Proof search
Citation
Collections
Source
Advances in Modal Logic, Volume 7
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
DOI
Restricted until
2037-12-31
Downloads
File
Description