f BBednarczyk - About me

Employment

Education

Awards

  • 2023
    Best student paper award at JELIA 2023 for the paper "Beyond ALCreg: Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features" (500 EURO + Eternal Glory).
  • 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

  • 2024
    DL 2025 (PC, Organizer), VLDB Summer School 2025 (Organizer), CSL 2025 (Reviewer), AAAI 2025 (PC)
  • 2024
    AAAI 2024 (PC), PODS 2024 (Reviewer), DL 2024 (PC), Logic Journal of the IGPL (Reviewer), LMCS (Reviewer), IJCAI 2024 (PC), KR 2024 (PC), SN Computer Science (Reviewer), AIML 2024 (Reviewer), Artificial Intelligence (Reviewer), Information and Computation (Reviewer)
  • 2023
    AAAI 2023 (PC), KR 2023 (PC), JELIA 2023 (PC, organizer), IJCAI 2023 (PC), DL 2023 (PC), DPFO Workshop 2023 (PC), TIME 2023 (PC), EUMAS 2023 (Reviewer)
  • 2022
    IJCAI 2022 (PC), KR 2022 (PC), DL 2022 (PC), CSL 2022 (Reviewer), LMCS (Reviewer), IPL (Reviewer), JAIR (Reviewer), ToCL (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

I actively supervise ambitious students, teaching them how to do research and often writing joint research papers with them. So far my students published their thesises at WOLLIC 2022, DL Workshop 2022, and FSTTCS 2021. Contact me if you are interested in doing some student (research) project together!

Finite Model Property for Hybrid Graded Mu-calculus

by Mikołaj Swoboda (BSc Thesis, defended 09.09.2024)

Abstract

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.

A Constructive Proof of a Van Benthem Theorem for the Forward Guarded Fragment of First Order Logic

by Benno Fünfstück (MSc Thesis, defended 24.06.2024)

Abstract

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.

Resolution for Forward Guarded Fragment

by Karol Ochman-Milarski (BSc Thesis, defended 10.02.2023)

Abstract

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.

E-learning platform supporting studying for the Matura exam in Computer Science

by Julita Osman, Aleksandra Stępniewska, Nikola Wrona (BEng Thesis, defended 10.02.2023)

Abstract

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.

Categorical semantics for model comparison games for description logics

by Mateusz Urbańczyk (MSc Thesis, 26th of October 2022)

Abstract

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.

Interpolation for the Two-Variable Guarded Fragment with Counting

by Johannes Tantow (Großer Beleg, defended 19th of October 2022)

Abstract

The main theorem of the project is the proof that the two-variable guarded fragment with counting quantifiers enjoys the Craig Interpolation Property.

Presburger Tree Automata With Applications to Logics With Expressive Counting

by Oskar Fiuk (BSc Thesis, defended 09.09.2022)

Abstract

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.

On Several Equivalent Characterisations of the Variety R

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

Abstract

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)

Abstract

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)

Abstract

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.