Bartosz Bednarczyk

KR Conference 2025 Conference Paper

Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards

• Bartosz Bednarczyk
• Emanuel Kieroński

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.

IJCAI Conference 2024 Conference Paper

Data Complexity in Expressive Description Logics with Path Expressions

• Bartosz Bednarczyk

We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a. k. a. ALCHbSelfregOIQ) 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.

JELIA Conference 2023 Conference Paper

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

• Bartosz Bednarczyk

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 \(\mathcal {ALC}_{\textsf {vpl}}\), an extension of \(\mathcal {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 \(\mathcal {ALC}_{\textsf {vpl}}\) with the seemingly innocent \(\textsf{Self}\) operator. Then, we consider the simplest non-regular (visibly-pushdown) language \( r ^\# s ^\# {: }{=}\{ r ^n s ^n \mid n \in \mathbb {N}\}\). We establish undecidability of the concept satisfiability problem for \({\mathcal {A}\mathcal {L}\mathcal {C}}_{\textsf {reg}}\) extended with nominals and \( r ^\# s ^\#\), as well as of the query entailment problem for \(\mathcal {ALC}\) -TBoxes, where such non-regular atoms are present in queries.

JAIR Journal 2023 Journal Article

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

• Bartosz Bednarczyk
• Sebastian Rudolph

It is commonly known that the conjunctive query entailment problem for certain extensions 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 several versions of the on 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 counter-intuitive 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.

AAAI Conference 2022 Conference Paper

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

• Bartosz Bednarczyk
• Emanuel Kieroński

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.

AAAI Conference 2022 Conference Paper

The Price of Selfishness: Conjunctive Query Entailment for ALCSelf Is 2EXPTIME-Hard

• Bartosz Bednarczyk
• Sebastian Rudolph

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 rolehierarchies) 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.

MFCS Conference 2022 Conference Paper

Towards a Model Theory of Ordered Logics: Expressivity and Interpolation

• Bartosz Bednarczyk
• Reijo Jaakkola

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.

JELIA Conference 2021 Conference Paper

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

• Bartosz Bednarczyk

Abstract We study the complexity of two standard reasoning problems for Forward Guarded Logic ( \(\mathcal {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 \(\mathcal {FGF}\) enjoys the higher-arity-forest-model property, which results in \(\textsc {ExpTime}\) -completeness of its (finite and unrestricted) knowledge-base satisfiability problem. Moreover, we show that \(\mathcal {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 \(\mathcal {FGF}\) remains in \(\textsc {ExpTime}\). We find that our results are quite unusual as \(\mathcal {FGF}\) is, up to our knowledge, the first decidable fragment of First-Order Logic, extending standard description logics like \(\mathcal {ALC}\), that offers unboundedly many variables and higher-arity relations while keeping its complexity surprisingly low.

IJCAI Conference 2020 Conference Paper

A Framework for Reasoning about Dynamic Axioms in Description Logics

• Bartosz Bednarczyk
• Stephane Demri
• Alessio Mansutti

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.

TIME Conference 2020 Conference Paper

A Note on C² Interpreted over Finite Data-Words

• Bartosz Bednarczyk
• Piotr Witkowski 0001

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 C²[≤, 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 [Angelo Montanari et al. , 2016]. We supplement our results with decidability for several sub-fragments of C²[≤, 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.

IJCAI Conference 2020 Conference Paper

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

• Bartosz Bednarczyk
• Robert Ferens
• Piotr Ostropolski-Nalewaja

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.

TCS Journal 2020 Journal Article

One-variable logic meets Presburger arithmetic

• Bartosz Bednarczyk

ECAI Conference 2020 Conference Paper

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

• Franz Baader
• Bartosz Bednarczyk
• Sebastian Rudolph

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.

JELIA Conference 2019 Conference Paper

On the Complexity of Graded Modal Logics with Converse

• Bartosz Bednarczyk
• Emanuel Kieronski
• Piotr Witkowski 0001

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.

IJCAI Conference 2019 Conference Paper

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

• Bartosz Bednarczyk
• Sebastian Rudolph

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 2EXPTIME-complete 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 first-order logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

CSL Conference 2017 Conference Paper

Extending Two-Variable Logic on Trees

• Bartosz Bednarczyk
• Witold Charatonik
• Emanuel Kieronski

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.