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éphane 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.
From October 2018 till September 2022 I was 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 title. In April 2019 I became a PHD student of Sebastian Rudolph at TU Dresden. My PHD defence took place on the 25th of June 2024 and I defended it with distinction (certificate). 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).
I plan to devote the forthcoming academic year (2024/25) to the project of solving a few open problems related to propositional dynamic logic and friends. In early 2025 I plan to apply for a three year FWF project at TU Wien, dedicated to further investigation of complexity and (finite) model theory ``ordered'' fragments of first-order logic. I am looking for prospective Master and PhD students, so drop me a line if you are interested in joint research.
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 (Dr. rer. nat.) in Computer Science
TU Dresden
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
Mu-calculus is a robust modal logic used in computer science for expressing and analyzing properties of transition systems. It extends basic modal logic by introducing fixed point operators, which allow for the expression of complex recursive properties in a compact and rigorous manner. The goal of this thesis is to explore the model-theoretic properties of mu-calculus extended with nominals (constants) and graded modalities (counting)—features commonly found in expressive ontology languages like OWL2 by W3C. We demonstrate that the resulting logic, known as hybrid graded mucalculus, possesses the finite model property (FMP), meaning that every satisfiable formula in this logic can be satisfied in a finite Kripke structure. Our proof is based on a detailed examination of the existing FMP proof for hybrid mu-calculus by Tamura, highlighting how his construction can be adapted to accommodate graded modalities. Additionally, we provide a complete proof of the correspondence between (hybrid) graded mu-calculus and parity games, a result initially announced by Kupferman, Vardi, and Sattler in 2002 but never proven in full detail.
The forward guarded fragment (FGF) is a recently introduced decidable fragment of first-order logic (FO) whose satisfiability problem is only ExpTime-complete. FGF derives from the guarded fragment (GF) by adding a restriction on the order in which variables may appear in for- mulae, similar to the fluted fragment by Purdy. FGF is a higher-arity generalization of multi-modal logic with global modalities, but in contrast to GF, it does not capture logics with inverse modalities. In total analogy to the classic van Benthem characterization of modal logic, we show that FGF is exactly the fragment of FO which consists of formulae that are invariant under a suitable notion of bisimulation for FGF. Crucially, we employ techniques by Martin Otto originally designed for modal logic which also work if we restrict the class of models under consideration to finite models only. In the process, we develop a new notion of unraveling for FGF, which produces tree-like models that satisfy the same FGF formulae as the original model. The new notion of unraveling is closely linked to a notion of unraveling for GF and is interesting on its own. As an application for our van Benthem style characterization, we show that whether a given GF has an equivalent formula in FGF is decidable.
The Guarded Fragment is a decidable fragment of first-order logic. We are concerned with a further restriction of the Guarded Fragment, called the Forward Guarded Fragment, in which variables appear in atoms only in the order of quantification. The Guarded Fragment can be decided with the resolution method in the double exponential time. We show that the resolution method for the Guarded Fragment can be used to decide Forward Guarded Fragment in single exponential time and we provide the implementation.
In this paper, we describe the concept and implementation of an online educational platform that offers materials designed to prepare for the matura exam in information technology at an extended level. We observed a shortage of similar sources of knowledge what is confirmed by the statistics provided by the Central Examination Commission every year. These statistics show that not only still a very small percentage of high school graduates decide to take the extended matura exam in computer science, but also their results are not very high. It is our ambition to contribute to change in this state of affairs. The platform’s course is divided into four parts: theory, Excel, Access and Python-based programming. Sound knowledge in each of these sections is crucial to get a high score in the high school graduation exam. For this reason, special emphasis was placed on a thorough study of each topic that may appear in the matura exam. The main goal was to build a platform that would help both students who are starting from scratch and those who have had the opportunity to study at school in preparation for the matura exam, regardless of the teaching level. All sections' topics are covered in detail and enriched by graphics to make learning more interesting and easier. In addition, each part has a section devoted to solving matura exam tasks and exercises for students to do on their own. This will allow the student to check whether he or she has already mastered a given range of material and will help to consolidate the acquired knowledge. Each topic in the programming part includes a list of tasks and their model solution. Additionally, the learning of this material is supported by a programming environment and a checker based on it, which is available on the site. The entire platform is written in React, one of the most popular and efficient frameworks for developing front-end applications. Its flexibility is a fast and efficient means for interactive and modern user experience. In addition, React is supported by a large community of developers, so as to provide access to a wide range of tools and libraries, which facilitate the development of functional and attractive websites.
A categorical approach to study model comparison games in terms of comonads was recently initiated by Abramsky et al. In this work, we analyse games that appear naturally in the context of description logics and supplement them with suitable game comonads. More precisely, we consider expressive sublogics of ALC Self IbO, namely, the logics that extend ALC with any combination of inverses, nominals, safe boolean roles combinations, and Self operator. Our construction augments and modifies the so-called modal comonad by Abramsky and Shah. The approach that we took heavily relies on the use of relative comonads, which we leverage to encapsulate additional capabilities within the bisimulation games in a compositional manner.
We introduce two versions of Presburger Automata with the Büchi acceptance condition, working over infinite, finite-branching trees. These automata, in addition to the classical ones, allow nodes for checking linear inequalities over labels of their children. We establish tight NP and ExpTime bounds on the complexity of the non-emptiness problem for the presented machines. We demonstrate the usefulness of our automata models by polynomially encoding the two-variable guarded fragment extended with Presburger constraints, improving the existing triply-exponential upper bound to a single exponential. This bachelor's thesis is based on joint work with Bartosz Bednarczyk, published at WOLLIC 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.
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.