Proof search and counter-model construction for bi-intuitionistic propositional logic

Luís Pinto

Departamento de Matemática
Universidade do Minho

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.)

Tarmo Uustalu
Last update 17.4.2010