Publications

Peer-reviewed papers and theses from 2017–2026, newest first. You can also check my publications on DBLP and Google Scholar.

Research themes

Click a theme to filter the list.

Dynamic logics and finite satisfiability

Propositional dynamic logic and its extensions with loops, intersection and converse, non-regular programs and regular guards. My current focus is finite satisfiability: deciding whether a formula has a finite model, the central question of my FWF project FINGO.

Key paperBeyond ALCreg: Exploring Non-Regular Extensions of PDL with Description Logics FeaturesJELIA 2023 · best student paper
Show these papers

Guarded, fluted and adjacent fragments

Fragments of first-order logic tamed by guards or by the order in which variables are quantified: guarded, forward, fluted, ordered and adjacent. I map where their decidability ends, pin down their complexity and study their model theory, including expressive power and interpolation.

Key paperOn the Limits of Decision: the Adjacent Fragment of First-Order LogicICALP 2023
Show these papers

Two-variable logic and counting

The one- and two-variable fragments extended with counting: exact, modulo and percentage quantifiers, frequencies and Presburger constraints, over arbitrary structures as well as words, trees and data words. Recurring tools are integer programming and tree automata with arithmetic.

Key paperOn Classical Decidable Logics extended with Percentage Quantifiers and ArithmeticsFSTTCS 2021
Show these papers

Description logics and query answering

Expressive description logics as ontology languages for querying data: the complexity of conjunctive query entailment, data complexity, path expressions, self-loops, cardinality constraints and statistical semantics, together with termination of the chase for existential rules.

Key paperHow to Tell Easy from Hard: Complexity of Conjunctive Query Entailment in Extensions of ALCJAIR 2023
Show these papers

Modal and temporal logics on trees

Modal and temporal logics interpreted over trees and forests: how propositional quantification, composition of models and graded or converse modalities affect expressive power and computational complexity, with links to separation logic and game comonads.

Key paperWhy Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?LMCS 2022
Show these papers
Sort by year
20262 papers
WorkshopDL 2026

Baby Steps Towards Finite Satisfiability for LoopPDL

Bartosz Bednarczyk, Mikołaj Swoboda
Proceedings of the 39th International Workshop on Description Logics (DL 2026)
PDFPublisher

Abstract

Propositional Dynamic Logic (PDL), known in the Description Logic community as ALCreg, is a well-established modal logic of programs. To increase its expressive power, several extensions have been proposed. One such extension is the loop operator, which expresses that an element can reach itself via a path defined by a regular expression. Although the satisfiability problem for LoopPDL is well understood, the decidability of its finite satisfiability problem has remained open for over 40 years. Our ongoing work aims to resolve this question. While a full solution is still pending, we have obtained some results of independent interest. In this workshop paper, we present a simplified version of our approach, applied to a logic with loops restricted to atomic roles and their transitive closures.

WorkshopDL 2026

A Horn Extension of DL-Lite with NL Data Complexity

Janos Arpasi, Bartosz Bednarczyk, Magdalena Ortiz
Proceedings of the 39th International Workshop on Description Logics (DL 2026)
PDFPublisher

Abstract

The literature on ontology-mediated query answering (OMQA) has been shaped by two key results: first-order rewritability for DL-Lite, and PTime-hardness of data complexity for essentially every description logic beyond it. This has effectively positioned DL-Lite as the only practical choice for query rewriting, restricting OMQA solutions to first-order queries and ontologies that can be rewritten into them. This AC0 vs. PTime dichotomy is especially limiting if we consider that OMQA targets graph-structured data, and that standard graph query languages (including the recent ISO standards GQL and SQL/PGQ) are typically NL-complete. Towards identifying a rich Horn DL that can be rewritten into graph query languages and that can still express many ELI and DL-Lite ontologies, we introduce a stratification mechanism for ELI that controls the interaction between conjunction and recursion. In this way, we obtain ELHI ⊥ ⪯ , a description logic that strictly extends the core DL-Lite, supports reachability axioms and restricted conjunction, and allows for reasoning in NL. We establish the NL upper bound via a rewriting into nested two-way regular path queries, a fragment of GQL, providing initial evidence that our ontology language is a promising candidate for extending OMQA to graph query languages.

20254 papers
ConferenceKR 2025

Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards

Bartosz Bednarczyk, Emanuel Kieroński
Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025)
arXivDOISlides

Abstract

We study the Guarded Fragment with Regular Guards RGF which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2ExpTime-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying the maximal, in some natural sense, ExpSpace-complete fragment of RGF.

WorkshopDL 2025

Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Abstract)

Bartosz Bednarczyk, Emanuel Kieroński
Proceedings of the 38th International Workshop on Description Logics (DL 2025)
PDFPublisher

Abstract

We study the Guarded Fragment with Regular Guards RGF which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2ExpTime-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying the maximal, in some natural sense, ExpSpace-complete fragment of RGF.

JournalJLC

The Adjacent Fragment and Quine’s Limits of Decision

Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann
Journal of Logic and Computation (JLC)
PDFDOI

Abstract

We introduce the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) the two-variable fragment of firstorder logic as well as the so-called fluted fragment. We show that the adjacent fragment has the finite model property, and that the satisfiability problem for its k-variable sub-fragment is in (k−1)-NExpTime. Using known results on the fluted fragment, it follows that the satisfiability problem for the whole adjacent fragment is Tower-complete. We additionally consider the effect of the adjacency requirement on the well-known guarded fragment of first-order logic, whose satisfiability problem is 2ExpTime-complete. We show that the satisfiability problem for the intersection of the adjacent and guarded adjacent fragments remains 2ExpTime-hard. Finally, we show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable.

JournalLMCS

About the Expressive Power and Complexity of Order-Invariance with Two Variables

Bartosz Bednarczyk, Julien Grange
Logical Methods in Computer Science (LMCS)
PDFDOI

Abstract

Order-invariant first-order logic is an extension of first-order logic (FO) where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity and expressive power. We first establish coNExpTime-completeness for the problem of deciding if a given two-variable formula is order-invariant, which tightens and significantly simplifies the coN2ExpTime proof by Zeume and Harwath. Second, we address the question of whether every property expressible in order-invariant two-variable logic is also expressible in first-order logic without the use of a linear order. While we were not able to provide a satisfactory answer to the question, we suspect that the answer is ``no''. To justify our claim, we present a class of finite tree-like structures (of unbounded degree) in which a relaxed variant of order-invariant two-variable FO expresses properties that are not definable in plain FO. On the other hand, we show that if one restricts their attention to classes of structures of bounded degree, then the expressive power of order-invariant two-variable FO is contained within FO.

20245 papers
ThesisPhD

Database-Inspired Reasoning Problems in Description Logics With Path Expressions

Bartosz Bednarczyk
TU Dresden
Advisors: Sebastian Rudolph & Emanuel Kieroński · Defended June 25, 2024
PDFPublisherSlides

Abstract

Formal ontologies are of significant importance in artificial intelligence, playing a central role in the Semantic Web, ontology-based information integration, or peer-to-peer data management. In such scenarios, an especially prominent role is played by description logics (DLs) – a robust family of logical formalisms used to describe ontologies and serving as the logical underpinning of contemporary standardised ontology languages. To put knowledge bases to full use as core part of intelligent information systems, much attention is being devoted to the area of ontology-based data-access, with conjunctive queries and their generalisations such as positive conjunctive two-way regular path queries being employed as a fundamental querying formalism. The most expressive exemplars of description logics feature advanced constructors for roles and path expressions. Among the most powerful knowledge representation formalisms on the verge of decidability, are the DLs from the Z family. For its most expressive proponent, ZOIQ (a.k.a. ALCHb Self reg OIQ), featuring nominals (O), role inverses (I), and number restrictions (Q), querying is undecidable and even decidability of knowledge-base satisfiability is open, owing to the intricate interplay of the three mentioned features. Restricting the interaction of O, I, and Q however (or excluding one of the features altogether) leads to beneficial model-theoretic properties, which give rise to upper bounds of ExpTime for knowledge-base satisfiability and 2ExpTime for querying. Aiming for better understanding of the “expressive power versus computational complexity” trade-off for the Z family of DLs, we provide a more fine-grained complexity analysis for the query entailment problem over ontologies. In the thesis we focus on tame fragments of ZOIQ, namely the fragments in which either one the three features from {I, O, Q} is dropped or the class of models is restricted to the so-called quasi-forests. We employ the query languages ranging from (unions of) conjunctive queries ((U)CQs) to positive two-way regular path queries (P2RPQs). We mostly follow the classical semantics of entailment, but we also provide several results in the “finite-model” scenario. The most important results of the thesis are summarised below. 1. We provide a complete classification of the complexity of the query entailment problem (for various query languages discussed above) for tamed fragments of ZOIQ under the classical semantics. This involves several new ingredients such as: (i) a uniform exponential-time algorithm based on Lutz’s spoiler technique for the entailment of unions of conjunctive queries for ALCHbreg, (ii) new lower bounds for (rooted and unrooted) conjunctive query entailment over ALCSelf ontologies, and (iii) a novel reduction from the entailment of P2RPQs to the satisfiability problem for tamed ZOIQ, yielding a uniform 2ExpTime upper bound for all the considered logics. As a preliminary step towards lifting the above results to the realm of data complexity, we establish that the satisfiability of tamed ZOIQ is NP-complete. 2. Under the finite model semantics, we focus on UCQs only. With the proviso that the finite satisfiability problem for ZIQ is ExpTime-complete, we also provide a complete picture of the complexity of the query entailment problems. The key insight is that ZOI and ZOQ are finitely controllable. 3. We conclude the thesis by investigating the decidability border of further extensions of the Z family of DLs. Our goal is to understand whether the class of regular languages present in path expressions in Z is maximal for guaranteeing decidability of the underlying logic. We provide a series of undecidability results involving simple, non-regular languages (a subclass of visibly pushdown languages). Our proofs rely on well-established model- and graph-theoretic definitions. What is more, most of them generalise (in a uniform way) and solidify multiple results known by the DL community. Our proofs are also easily adjustable to freshly defined logics, without the need to reproduce nearly-identical proofs.

ConferenceIJCAI 2024

Data Complexity in Expressive Description Logics With Path Expressions

Bartosz Bednarczyk
Proceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI 2024)
PDFDOISlides

Abstract

We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb^self_regOIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape for decidable fragments of ZOIQ, and reproves known results on decidable fragments of OWL2 (SR family). Using the same technique, we establish coNExpTime-completeness (w.r.t. the combined complexity) of the entailment problem of rooted queries in ZIQ.

WorkshopDL 2024

Data Complexity in Expressive Description Logics With Path Expressions (Extended Abstract)

Bartosz Bednarczyk
Proceedings of the 37th International Workshop on Description Logics (DL 2024)
PDFPublisher

Abstract

We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb^self_regOIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape for decidable fragments of ZOIQ, and reproves known results on decidable fragments of OWL2 (SR family). Using the same technique, we establish coNExpTime-completeness (w.r.t. the combined complexity) of the entailment problem of rooted queries in ZIQ.

WorkshopDL 2024

On the Limits of Decision: the Adjacent Fragment of First-Order Logic (Extended Abstract)

Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann
Proceedings of the 37th International Workshop on Description Logics (DL 2024)
PDFPublisher

Abstract

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

JournalLMCS

Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

Bartosz Bednarczyk
Logical Methods in Computer Science (LMCS)
arXivDOI

Abstract

We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALCvpl, was introduced and investigated by Loding and Serre in 2007. The logic ALCvpl generalises many known decidable non-regular extensions of ALCreg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALCvpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r#s# := { r^n s^n | n in N } for fixed role names r and s. Finally, in contrast to the classical database setting, we establish undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes.

20234 papers
JournalJAIR

How to Tell Easy from Hard: Complexity of Conjunctive Query Entailment in Extensions of ALC

Bartosz Bednarczyk, Sebastian Rudolph
Journal of Artificial Intelligence Research (JAIR)
PDFDOI

Abstract

It is commonly known that the conjunctive query entailment problem for certain ex- tensions of (the well-known ontology language) ALC is computationally harder than their knowledge base satisfiability problem while for others the complexities coincide, both under the standard and the finite-model semantics. We expose a uniform principle behind this divide by identifying a wide class of (finitely) locally-forward description logics, for which we prove that (finite) query entailment problem can be solved by a reduction to exponentially many calls of the (finite) knowledge base satisfiability problem. Consequently, our algorithm yields tight ExpTime upper bounds for locally-forward logics with ExpTime-complete knowledge base satisfiability problem, including logics between ALC and μALCHbregQ (and more), as well as ALCSCC with global cardinality constraints, for which the complexity of querying remained open. Moreover, to make our technique applicable in future research, we provide easy-to-check sufficient conditions for a logic to be locally-forward based on several novel versions of the model-theoretic notion of unravellings. Together with existing results, this provides a nearly complete classification of the “benign” vs. “malign” primitive modelling features extending ALC, missing out only the Self operator. We then show a rather surprising result, namely that the conjunctive entailment problem for ALCSelf is exponentially harder than for ALC. This places the seemingly innocuous Self operator among the “malign” modelling features, like inverses, transitivity or nominals.

ConferenceJELIA 2023 Best student paper award

Beyond ALCreg: Exploring Non-Regular Extensions of PDL with Description Logics Features

Bartosz Bednarczyk
Proceedings of the 18th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2023)
PDFDOISlides

Abstract

We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics. Our primary object of interest is ALCvpl, an extension of ALC with path expressions using visibly-pushdown languages, which was shown to be decidable by Löding et al. in 2007. The paper present a series of undecidability results. We prove undecidability of ALCvpl with the seemingly innocent Self operator. Then, we consider the simplest non-regular (visibly-pushdown) language r#s# := {rnsn | n ∈ N}. We establish un- decidability of the concept satisfiability problem for ALCreg extended with nominals and r#s#, as well as of the query entailment problem for ALC-TBoxes, where such non-regular atoms are present in queries.

ConferenceICALP 2023

On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann
Proceedings of the 50th EATCS International Colloquium on Automata, Languages and Programming (ICALP 2023)
PDFDOI

Abstract

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

JournalACM TOCL

On Composing Finite Forests with Modal Logics

Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
ACM Transactions on Computational Logic
PDFDOI

Abstract

We study the expressivity and complexity of two modal logics interpreted on inite forests and equipped with standard modalities to reason on submodels. The logic ML( ) extends the modal logic K with the composition operator from ambient logic, whereas ML(∗) features the separating conjunction ∗ from separation logic. Both operators are second-order in nature. We show that ML( ) is as expressive as the graded modal logic GML (on trees) whereas ML(∗) is strictly less expressive than GML. Moreover, we establish that the satisfiability problem is Tower-complete for ML(∗), whereas it is (only) AExpPolcomplete for ML( ), a result which is surprising given their relative expressivity. As by-products, we solve open problems related to sister logics such as static ambient logic and modal separation logic.

20226 papers
JournalLMCS

Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

Bartosz Bednarczyk, Stéphane Demri
Logical Methods in Computer Science
PDFDOI

Abstract

Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that tQCTL restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When tQCTL restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.

ConferenceWoLLIC 2022

Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting

Bartosz Bednarczyk, Oskar Fiuk
Proceedings of the 28th Workshop on Logic, Language, Information and Computation (WOLLIC 2022)
PDFDOI

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.

ConferenceMFCS 2022

Towards Model Theory of Ordered Logics: Expressivity and Interpolation

Bartosz Bednarczyk, Reijo Jaakkola
Proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
PDFarXivDOISlides

Abstract

We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO à la van Benthem. Afterwards, we study the Craig Interpolation Property (CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the ``forwardness'' of our logics.

WorkshopDL 2022

Comonadic Semantics for Description Logics Games

Bartosz Bednarczyk, Mateusz Urbańczyk
Proceedings of the Description Logics Workshop 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 ALCSelf IbO, namely, the logics that extend ALC with any combination of inverses, nominals, safe boolean roles combinations and the 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 monads, which we leverage to encapsulate additional capabilities within the bisimulation games in a compositional manner.

ConferenceAAAI 2022

Finite Entailment of Local Queries in the Z Family of Description Logics

Bartosz Bednarczyk, Emanuel Kieroński
Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI 2022)
PDFDOISlidesVideo

Abstract

In the last few years the field of logic-based knowledge representation took a lot of inspiration from database theory. A vital example is that the finite model semantics in description logics (DLs) is reconsidered as a desirable alternative to the classical one and that query entailment has replaced knowledge-base satisfiability (KBSat) checking as the key inference problem. However, despite the considerable effort, the overall picture concerning finite query answering in DLs is still incomplete. In this work we study the complexity of finite entailment of local queries (conjunctive queries and positive boolean combinations thereof) in the Z family of DLs, one of the most powerful KR formalisms, lying on the verge of decidability. Our main result is that the DLs ZOQ and ZOI are finitely controllable, i.e. that their finite and unrestricted entailment problems for local queries coincide. This allows us to reuse recently established upper bounds on querying these logics under the classical semantics. While we will not solve finite query entailment for the third main logic in the Z family, ZIQ, we provide a generic reduction from the finite entailment problem to the finite KBSat problem, working for ZIQ and some of its sublogics. Our proofs unify and solidify previously established results on finite satisfiability and finite query entailment for many known DLs.

ConferenceAAAI 2022

The Price of Selfishness: Conjunctive Query Entailment for ALCSelf is 2ExpTime-Hard

Bartosz Bednarczyk, Sebastian Rudolph
Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI 2022)
PDFDOISlidesVideo

Abstract

Abstract: In logic-based knowledge representation, query answering has essentially replaced mere satisfiability checking as the inferencing problem of primary interest. For knowledge bases in the basic description logic ALC, the computational complexity of conjunctive query (CQ) answering is well known to be EXPTIME-complete and hence not harder than satisfiability. This does not change when the logic is extended by certain features (such as counting or role hierarchies), whereas adding others (inverses, nominals or transitivity together with role-hierarchies) turns CQ answering exponentially harder. We contribute to this line of results by showing the surprising fact that even extending ALC by just the Self operator – which proved innocuous in many other contexts – increases the complexity of CQ entailment to 2ExpTime. As common for this type of problem, our proof establishes a reduction from alternating Turing machines running in exponential space, but several novel ideas and encoding tricks are required to make the approach work in that specific, restricted setting.

20217 papers
ConferenceFSTTCS 2021

On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics

Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, Tony Tan
Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)
PDFDOISlidesVideo

Abstract

During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first-order fragments are too weak to express even the simplest statistical constraints, required for modelling of influence networks or in statistical reasoning. In this work we investigate the extensions of these classical decidable logics with percentage quantifiers, specifying how frequently a formula is satisfied in the indented model. We show, surprisingly, that all the mentioned decidable fragments become undecidable under such extension, sharpening the existing results in the literature. Our negative results are supplemented by decidability of the two-variable guarded fragment with even more expressive counting, namely Presburger constraints. Our results can be applied to infer decidability of various modal and description logics, e.g. Presburger Modal Logics with Converse or ALCI, with expressive cardinality constraints.

WorkshopDL 2021

The Price of Selfishness: Conjunctive Query Entailment for ALCSelf is 2ExpTime-hard (Extended Abstract)

Bartosz Bednarczyk, Sebastian Rudolph
Proceedings of the Description Logics Workshop 2021
arXivExtended abstractSlides
WorkshopDL 2021

Finite-Controllability of Conjunctive Queries in the Z family of Description Logics (Extended Abstract)

Bartosz Bednarczyk, Emanuel Kieroński
Proceedings of the Description Logics Workshop 2021
Extended abstractSlides
JournalTPLP

Completing the Picture: Complexity of Graded Modal Logics with Converse

Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski
Theory and Practice of Logic Programming
arXivDOI

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have already been established. By ”traditional” classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

JournalIPL

Statistical EL is ExpTime-complete

Bartosz Bednarczyk
Information Processing Letters
arXivDOI

Abstract

We show that the consistency problem for Statistical EL ontologies, defined by Penaloza and Potyka in SUM 2017, is ExpTime-hard. Together with existing ExpTime upper bounds, we conclude ExpTime-completeness of the logic. Our proof goes via a reduction from the consistency problem for EL extended with negation of atomic concepts.

ConferenceJELIA 2021 Best student paper award

Exploiting forwardness: Satisfiability and Query-Entailment in Forward Guarded Fragment

Bartosz Bednarczyk
Proceedings of the 17th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2021)
PDFDOISlides

Abstract

We study the complexity of two standard reasoning problems for Forward Guarded Logic (FGF), obtained as a restriction of the Guarded Fragment in which variables appear in atoms only in the order of their quantification. We show that FGF enjoys the higher-arity-forest- model property, which results in ExpTime-completeness of its (finite and unrestricted) knowledge-base satisfiability problem. Moreover, we show that FGF is well-suited for knowledge representation. By employing a generalisation of Lutz’s spoiler technique, we prove that the conjunctive query entailment problem for FGF remains in ExpTime. We find that our results are quite unusual as FGF is, up to our knowledge, the first decidable fragment of First-Order Logic, extending standard description logics like ALC, that offers unboundedly many variables and higher-arity relations while keeping its complexity surprisingly low.

ConferenceFoSSaCS 2021

“Most of” leads to undecidability: Failure of adding frequencies to LTL

Bartosz Bednarczyk, Jakub Michaliszyn
Proceedings of the 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021)
arXivDOISlidesVideo

Abstract

Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and briefly discuss how the undecidability results transfer to first-order logic on words.

20205 papers
ConferenceTIME 2020

A note on C2 interpreted over finite data-words

Bartosz Bednarczyk, Piotr Witkowski
Proceedings of the 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)
DOI

Abstract

We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C2[≤,succ,∼,πbin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from ,πbin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ~. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [MontanariPS16]. We supplement our results with decidability for several sub-fragments of C2[≤,succ,∼,πbin], e.g., without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant.

ConferenceIJCAI 2020

All-Instances Oblivious Chase Termination is Undecidable for Single-Head Binary TGDs

Bartosz Bednarczyk, Robert Ferens, Piotr Ostropolski-Nalewaja
Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI 2020)
PDFDOI

Abstract

The chase is a famous algorithmic procedure in database theory with numerous applications in ontology-mediated query answering. We consider static analysis of the chase termination problem, which asks, given set of TGDs, whether the chase terminates on all input databases. The problem was recently shown to be undecidable by Gogacz et al. for sets of rules containing only ternary predicates. In this work, we show that undecidability occurs already for sets of single-head TGD over binary vocabularies. This question is relevant since many real-world ontologies, e.g., those from the Horn fragment of the popular OWL, are of this shape.

ConferenceIJCAI 2020

A Framework for Reasoning about Dynamic Axioms in Description Logics

Bartosz Bednarczyk, Stéphane Demri, Alessio Mansutti
Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI 2020)
PDFDOISlidesVideo

Abstract

Description logics are well-known logical formalisms for knowledge representation. We propose to enrich knowledge bases (KBs) with dynamic axioms that specify how the satisfaction of statements from the KBs evolves when the interpretation is decomposed or recomposed, providing a natural means to predict the evolution of interpretations. Our dynamic axioms borrow logical connectives from separation logics, well-known specification languages to verify programs with dynamic data structures. In the paper, we focus on ALC and EL augmented with dynamic axioms, or to their subclass of positive dynamic axioms. The knowledge base consistency problem in the presence of dynamic axioms is investigated, leading to interesting complexity results, among which the problem for EL with positive dynamic axioms is tractable, whereas EL with dynamic axioms is undecidable.

ConferenceLICS 2020

Modal Logics with Composition on Finite Forests: Expressivity and Complexity

Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
PDFDOIVideo

Abstract

We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(∗) contains the separating conjunction ∗ from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(∗) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(∗) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete.As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.s

ConferenceECAI 2020

Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020)
DOITech reportSlidesVideo

Abstract

Abstract. We introduce and investigate the expressive description logic (DL) ALCSCC++, in which the global and local cardinality constraints introduced in previous papers can be mixed. We prove that the added expressivity does not increase the complexity of satisfiability checking and other standard inference problems. However, reasoning in ALCSCC++ becomes undecidable if inverse roles are added or conjunctive query entailment is considered. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted. In this setting, query entailment can be shown to be EXPTIME-complete and hence not harder than reasoning in ALC.

20196 papers
JournalTCS

One-Variable Logic Meets Presburger Arithmetic

Bartosz Bednarczyk
Theoretical Computer Science
arXivDOI

Abstract

We consider the one-variable fragment of first-order logic extended with Presburger constraints. The logic is designed in such a way that it subsumes the previously-known fragments extended with counting, modulo counting or cardinality comparison and combines their expressive powers. We prove NP-completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem.

ConferenceIJCAI 2019

Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

Bartosz Bednarczyk, Sebastian Rudolph
Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 2019
PDFDOISlides

Abstract

Among the most expressive knowledge representation formalisms are the description logics of the Z family. For well-behaved fragments of ZOIQ, entailment of positive two-way regular path queries is well known to be 2EXPTIMEcomplete under the proviso of unary encoding of numbers in cardinality constraints. We show that this assumption can be dropped without an increase in complexity and EXPTIME-completeness can be achieved when bounding the number of query atoms, using a novel reduction from query entailment to knowledge base satisfiability. These findings allow to strengthen other results regarding query entailment and query containment problems in very expressive description logics. Our results also carry over to GC2 , the two-variable guarded fragment of firstorder logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

WorkshopDL 2019

Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

Bartosz Bednarczyk, Sebastian Rudolph
Proceedings of the Description Logics Workshop 2019
PDFPublisherSlides

Abstract

Among the most expressive knowledge representation formalisms are the description logics of the Z family. For well-behaved fragments of ZOIQ, entailment of positive two-way regular path queries is well known to be 2EXPTIMEcomplete under the proviso of unary encoding of numbers in cardinality constraints. We show that this assumption can be dropped without an increase in complexity and EXPTIME-completeness can be achieved when bounding the number of query atoms, using a novel reduction from query entailment to knowledge base satisfiability. These findings allow to strengthen other results regarding query entailment and query containment problems in very expressive description logics. Our results also carry over to GC2 , the two-variable guarded fragment of firstorder logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

WorkshopDL 2019

Satisfiability Checking and Conjunctive Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Proceedings of the Description Logics Workshop 2019
PDFPublisherSlides

Abstract

We consider an expressive description logic (DL) in which the global and local cardinality constraints introduced in previous papers can be mixed. On the one hand, we show that this does not increase the complexity of satisfiability checking and other standard inference problems. On the other hand, conjunctive query entailment in this DL turns out to be undecidable. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted.

ConferenceLICS 2019

Why propositional quantification makes modal logics on trees robustly hard?

Bartosz Bednarczyk, Stéphane Demri
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
PDFDOISlides

Abstract

Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability whereas CTL with propositional quantification under the tree semantics (written QCTLt) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTLt as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTLt restricted to the temporal operator EX is already Tower-hard, which is unexpected as, for instance, EX can only enforce local properties. When QCTLt restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExppol-complete; AExppol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As significant consequences of our proof method, we prove Tower-hardness of QCTLt restricted to EF or to EXEF and of the well-known modal logics K, KD, GL, S4, K4 and D4, with propositional quantification under a semantics based on classes of trees.

ConferenceJELIA 2019

On the Complexity of Graded Modal Logics with Converse

Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski
Proceedings of the 16th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2019)
arXivDOI

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames has already been established. By 'traditional' classes of frames we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

20181 paper
ThesisM1

Assertion Languages with Modalities and Separating Connectives

Bartosz Bednarczyk
ENS Paris-Saclay (MPRI)
Advisor: Stéphane Demri · Defended Sep. 7, 2018
PDFSlides

Abstract

Quantified Computation Tree Logic QCTL extends the well-known temporal logic CTL with quantification over atomic propositions. While the logic was defined long time ago, only quite recently it was shown to have a non-elementary satisfiability problem under tree semantics by Laroussinie and Markey in LMCS 2014. Motivated by this result, we tried to identify a natural fragment of QCTL enjoying an elementary complexity while allowing the full power of propositional quantification. We show that the most natural fragment of QCTL, containing only the EX modality, is already Tower-hard. That sharpens the hardness result for the full logic. Additionally, we turn our attention to a special case where tree models are of bounded degree and prove that the complexity drops to a class between NExpTime and ExpSpace.

20174 papers
ConferenceFSTTCS 2017

Modulo Counting on Words and Trees

Bartosz Bednarczyk, Witold Charatonik
Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11–15, 2017, Kanpur, India. LIPIcs 93, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages 12:1–12:16
PDFDOISlides

Abstract

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2ExpTime algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.

ConferenceCSL 2017

Extending Two-Variable Logic on Trees

Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieroński
Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden. LIPIcs 82, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages 11:1-11:20
PDFDOISlides

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

ConferenceESSLLI 2017 StuS

On One Variable Fragment of First Order Logic with Modulo Counting Quantifier

Bartosz Bednarczyk
Proceedings of ESSLLI 2017 Student Session, 29th European Summer School in Logic, Language & Information, July 17-28, 2017, Toulouse, France, pages 7-13
PDFPublisherSlides

Abstract

We consider the one-variable fragment of first-order logic extended with modulo counting quantifiers. We prove NPTime-completeness of such fragment by presenting an optimal algorithm for solving its finite satisfiability problem.

ThesisBSc

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

Bartosz Bednarczyk
University of Wrocław
Advisor: Witold Charatonik · Defended Feb. 15, 2017
PDFPublisher

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We show that adding counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem.

No publications match your search.