• PHD Student01.10.2018-01.04.2024

    PHD in Computer Science

    TU Dresden / University of Wrocław

    Supervisors: Sebastian Rudolph and Emanuel Kieroński

    Title: Database-Inspired Reasoning Problems in Description Logics With Path Expressions

  • M1 Computer Science01.09.2017-01.09.2018

    Master 1 voie Jacques Herbrand

    École normale supérieure Paris-Saclay

    Supervisor: Stéphane Demri

    Title: Assertion languages with modalities and separating connectives

  • BSc.01.10.2014 - 15.02.2017

    BSc. in Computer Science

    University of Wrocław

    Supervisor: Witold Charatonik

    Title: Satisfiability of the Two-Variable Fragment of First-Order Logic with counting quantifiers over finite trees


  • 2021
    Award for Outstanding Young Scientists from the Polish Ministry of Science and Higher Education (194 040 PLN).
  • 2021
    Best student paper award at JELIA 2021 for the paper "Exploiting Forwardness: Satisfiability and Query-Entailment in Forward Guarded Fragment" (500 EURO + Eternal Glory).
  • 2019
    Hugo Steinhaus Scholarship for Mathematical Sciences (for outstanding PHD Students from Wrocław, 18 000 PLN)
  • 2018
    Diamond Grant by the Polish Ministry of Science and Higher Education (prestigious funding for own 4 year project) for "Logics with generalized counting quantifiers for programs operating on data and database systems" (191 110 PLN).

Professional service

  • 2023
    AAAI 2023 (PC)
  • 2022
    IJCAI 2022 (PC), KR 2022 (PC), DL 2022 (PC), CSL 2022 (Reviewer), LMCS (Reviewer), IPL (Reviewer), JAIR (Reviewer)
  • 2021
    IJCAI 2021 (Senior PC), DL 2021 (Reviewer), Elsevier Artificial Intelligence (Reviewer), Fundamenta Informaticae (Reviewer)
  • 2020
    KR 2020 (Reviewer), CONCUR 2020 (Reviewer), DL 2020 (Reviewer)

Student supervision

Categorical semantics for model comparison games for description logics

by Mateusz Urbańczyk (MSc Thesis, ongoing work)

Presburger Tree Automata With Applications to Logics With Expressive Counting

by Oskar Fiuk (BSc Thesis, defended 09.09.2022)

On Several Equivalent Characterisations of the Variety R

by Sebastian Zięciak (BSc Thesis, defended February 2022)


One of a celebrated results in automata theory is that the notion of regularity in formal languages is robust in a very strong sense. More precisely, several equivalent characterisations of regular languages were given. It turns out that regular languages are precisely the languages recognisable by finite automata, finite monoids, regular expressions, and definable in the monadic second order logic. Similar characterisations are also known for the first-order definable languages, e.g. these are the languages recognisable by finite aperiodic monoids. Inspired by the algebraic approach to formal languages, we aim at describing the connection between languages recognizable by finite monoids from the variety R, and the suitable restrictions of first-order logic, regular expressions, finite automata, temporal logics and more.

Statistical constructions in decidable fragments of First-Order Logic

by Maja Orłowska and Anna Pacanowska (BSc Thesis, defended 28th June 2021)


In this thesis we consider first order logic extended with percentage quantifiers, allowing us to express statistical properties. Such quantifiers are defined under two different semantics: global and local. We show undecidability of the satisfiability problem for the extended two-variable fragment FO2 under both semantics, two-variable guarded fragment GF2 under the global semantics, as well as the three-variable guarded fragment GF3 (and hence the full GF) under the local semantics of percentage counting. We supplement our results with decidability status of the two-variable guarded fragment GF2 with local percentage counting and monadic fragment with global percentage counting.

The complexity of the satisfiability problem for Modal Logics with Data over Heaps

by Martyna Siejba (MSc Thesis, defended 17th March 2021)


Modal Logic with Data has been introduced by D.Baelde, S. Lunel and S. Schmitz for reasoning on simplified representation of XML trees. In this thesis we propose a variant of this logic interpreted over heaps with data, which we call Modal Logic with Data over Heaps. Our logic is more expansive than the logic from Modal Logic with Data: it allows for unbounded number of data values, inverse modalities and their transitive closures. We investigate the complexity of two selected fragments of the logic. The first fragment is a fragment with standard modalities and their inverses, but without their transitive closures. We prove it to be PSpace-complete. The PSpace-hardness goes by a reduction from standard modal logic. The PSpace upper bound is shown by a reduction to graded modal logic with inverse. In the second fragment under consideration the structures are accessed by the transitive closures of the inverse modalities but the basic modalities are not employed. The crux of the proof is showing the polynomial-depth model property of the logic. We first prove that every satisfiable formula has a model being a single tree and a loop. We then polynomially bound the size of the loop and the depth of the tree. Finally, we exponentially bound the branching factor of the tree. This leads to an NPSpace = PSpace algorithm for satisfiability testing. The PSpace-hardness is inherited from standard modal logic. We therefore obtain PSpace-completeness of the satisfiability problem.