arXiv subjects

Bartosz Jan Bednarczyk

Publications and source records attributed to Bartosz Jan Bednarczyk.

3 recordsLinked to original sources

arXiv2026

Two Variables and Two-Dimensional Structures

We study the two-variable fragment FO^2 of first-order logic over two-dimensional structures. Formulae may employ two linear orders <=_1, <=_2, their successor relations S_1, S_2, and auxiliary predicates of any arity. Despite two decades of work, three cases of finite satisfiability in this setting were still open; we settle all three. First, finite satisfiability of FO^2 with one linear order and one successor relation, of the same or of a different order, is NExpTime-complete, even with arbitrary auxiliary predicates and constant symbols. This closes a gap left open by Manuel and Zeume (CSL 2013). As an application, a reduction based on swaps of adjacent elements shows that order-invariance and order-successor-invariance of FO^2 are coNExpTime-complete. This reproves the main result of Zeume and Harwath (LICS 2016) and settles their question on order-successor-invariance. Second, finite satisfiability of FO^2 with two linear orders is ExpSpace-hard, already without auxiliary non-unary predicates, matching the upper bound known since 2010. Our reduction combines Kieronski's encoding of alternating Turing machines with the classical fact that the pre-order and post-order traversals of a tree define its descendant relation. Third, with two linear orders and the successor of one of them, finite satisfiability is in ExpSpace even with arbitrary auxiliary predicates, improving the previous 2NExpTime bound and confirming a conjecture of Zeume and Harwath. Together with known results, our theorems show that in two dimensions, auxiliary (non-unary) predicates and constants come for free: with or without them, the complexities coincide. All our proofs are simple.

cs.LO↗

arXiv2026

Towards Finite Satisfiability of PDL with Loops

Propositional Dynamic Logic (PDL) is a well-established modal logic of programs. Among its many extensions, the loop operator stands out for capturing the cyclic behaviour of programs: a world satisfies loop(pi) precisely when it can return to itself along a path matching the regular expression pi. While the satisfiability problem for the resulting logic LPDL was settled already in the 1980s, the decidability of its finite satisfiability problem has remained open ever since. The core difficulty is inherent to the finite setting: requiring and forbidding cycles at once is easily reconciled over arbitrary models, but over finite ones it defeats the existing finite-model-theoretic techniques. We make the first substantial progress towards closing this gap. We prove that finite satisfiability is ExpTime-complete for LPDL formulae (also in the presence of the converse operator) in negation normal form, under the restriction that every negated non-atomic loop has the form loop(pi^+) for some arbitrarily complex program pi -- a generalised form of self-reachability; positive occurrences of loops remain unrestricted. At the heart of our approach lies a novel way of representing intended finite models as their infinite, cactus-like unravellings: these are recognisable by two-way tree automata and satisfy a tailored omega-regular foldability condition that lets us finitise the accepted structures.

cs.LO↗

arXiv2026

A Horn extension of DL-Lite with NL data complexity

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 ELbotpreceq, 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.

cs.LO↗