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

Computer Science Laboratory

Australian National University

Thursday, 2 October 2008, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: Bi-intuitionistic logic is the extension
of intuitionistic logic with exclusion, a connective dual to
implication. Bi-intuitionistic logic was introduced by Rauszer as a
Hilbert calculus with algebraic and Kripke semantics. But her
subsequent "cut-free" sequent calculus has recently been shown by
Uustalu to fail cut-elimination.
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. 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. (Joint work with Rajeev Goré and Alwen
Tiu.)

Tarmo Uustalu

Last update 2.10.2008