I was born in 1995, in a small city called Strzelce Opolskie, where I attended the public primary school no. 7 as well as the local highschool and secondary school. In 2014 I moved to Wrocław, where I started joint math and computer science studies at the University of Wrocław. During my studies I worked as a teaching assistant for a student with disabilities (teaching programming in C and logic for computer scientists). On countless occasions, I also used to organise some auxiliary lessons dedicated to students having problems in passing the "logic for computer scientists" course. I also had a short period of being a programmer: I worked for three months in the company called Neurosoft in Wrocław (developing webapps in Groovy and MongoDB) as well as in Bloomberg in London (monitoring CassandraDB). I finished my BSc. studies defending my research-level thesis titled "Satisfiability of the Two-Variable Fragment of First-Order Logic with counting quantifiers over finite trees", supervised by Witold Charatonik (I consider him as my scientific father).
From March 2017 to the June 2018, I was employed in the NCN grant of Emanuel Kieroński, titled "A quest for new computer logics". During my employment I have managed to publish three papers ESSLLI 2017, CSL 2017 oraz FSTTCS 2017. In the meantime I did an internship in IST Austria (close to Vienna), where together with Krishnendu Chatterjee I worked on temporal logics for quantitative properties. In September 2017 I started my master studies in Cachan, where I finished my M1 level studies with honours (magna cum laude). My supervisor was Stéphan Demri and my M1 Master Thesis was published at LICS conference (the best logic conference in the world!). After finishing my M1 studies in Cachan I did a three month visit to the University of Oxford, where I worked with Michaël Cadilhac on tree algebras and their connections to circuit complexity.
Since October 2018 I am the PI in a Diamond Grant titled "Logics with generalized counting quantifiers for programs operating on data and database systems", which gave me an opportunity to start my PHD studies in Wrocław without having the full master degree. Since April 2019 I am also a PHD student of Sebastian Rudolph at TU Dresden. My PHD defence will take place in March 2024. My current research is about decidable fragments of first-order logic (including guarded fragments, fluted/ordered fragments, 2-variable fragments, description logics and temporal logics). I'm always tempted to try new things so my research is a bit diverse (at least in the area of logic).
Computer Science Department, University of Wrocław
Logics with generalized counting quantifiers for programs operating on data and database systems
A quest for new computer logics, PI: Emanuel Kieroński
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
Master 1 voie Jacques Herbrand
École normale supérieure Paris-Saclay
Supervisor: Stéphane Demri
Title: Assertion languages with modalities and separating connectives
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
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.
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.
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.