Friday, 9 April 2010, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Bi-intuitionistic logic is an extension of intuitionistic logic with a connective dual to implication (related to the set difference operator) that admits semantics in terms of Kripke structures and Heyting-Brouwer algebras.
Propositional bi-intuitionistic logic (BiInt) is decidable, but traditional sequent calculi formulations of it enjoying cut-elimination are not known, and the task of designing decision algorithms for the logic reveals intricacies.
In this seminar, after overviewing BiInt and the basics of proof search in sequent calculus, we present an adequate sequent calculus with labels for BiInt, alongside with a sound and complete algorithm for proof construction, which allows also extraction of Kripke counter-models for the non-theorems of BiInt.
(Joint work with Tarmo Uustalu.)