Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Satisfiability of Two-Variable Logics with Transitive or Equivalence Relations

  • Speaker:   Dr  Emanuel Kieronski  (University of Wroclaw)
  • Host:   Ian Pratt-Hartmann
  • 17th February 2010 at 14:15 in Lecture Theatre 1.4, Kilburn Building
Many logics appearing in various areas of computer science, eg. modal and description logics, are contained in (some variants or natural extensions of) the two-variable (FO2) and the guarded (GF) fragments of first order logic.

In applications of logics we very often require transitive or equivalence relations. Unfortunately, transitivity can be expressed neither in FO2 nor in GF. Thus, a natural idea (which comes from modal and description logics) is to consider satisfiability of FO2 and GF in special classes of models, in which some distinguished binary symbols have to be interpreted as transitive or equivalence relations.

In this talk I review some of the results from this area. I am going to concentrate on the case of finite satisfiability: given a logical formula check whether it has a finite model. In particular, I outline the decidability proof for GF2 with transitive or equivalence relations in guards.
▲ Up to the top