## 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