arxiv: 2605.13367 · v1 · submitted 2026-05-13 · 💻 cs.LO · cs.AI· cs.DB

Recognition: no theorem link

A Horn extension of DL-Lite with NL data complexity

Janos Arpasi , Bartosz Jan Bednarczyk , Magdalena Ortiz

Authors on Pith no claims yet

Pith reviewed 2026-05-14 18:45 UTC · model grok-4.3

classification 💻 cs.LO cs.AIcs.DB

keywords description logicsDL-Liteontology-mediated query answeringdata complexityregular path queriesHorn logicsgraph queriesNL complexity

0 comments

The pith

ELbotpreceq extends core DL-Lite with reachability axioms and restricted conjunction while keeping reasoning in NL data complexity.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper seeks a Horn description logic richer than DL-Lite that still supports efficient query answering on graph data. It adds a stratification mechanism to ELI that limits how conjunction interacts with recursive reachability axioms. The resulting ELbotpreceq strictly extends the core of DL-Lite yet admits a rewriting to nested two-way regular path queries. This rewriting places the data complexity in NL, matching the complexity of standard graph query languages. A sympathetic reader would see this as a step toward using ISO graph query standards such as GQL directly in ontology-mediated query answering.

Core claim

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.

What carries the argument

The stratification mechanism on ELI that controls the interaction between conjunction and recursion to preserve NL complexity.

If this is right

Reasoning reduces to evaluation of nested two-way regular path queries.
OMQA solutions can target graph query languages beyond first-order rewritability.
Many ELI and DL-Lite ontologies remain expressible while gaining reachability axioms.
Data complexity stays in NL even when recursion and limited conjunction are present.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar stratification techniques could be tested on other recursive query fragments to obtain NL bounds.
Direct embedding into graph database engines supporting GQL becomes plausible if the rewriting is efficient.
Further relaxations of the stratification rules might be checked for their effect on complexity.

Load-bearing premise

Stratification restricts conjunction-recursion interactions enough to keep data complexity in NL while still extending DL-Lite expressivity.

What would settle it

An ontology and query pair in ELbotpreceq whose answering problem lies outside NL would falsify the claimed upper bound.

read the original 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 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper defines a stratified ELI fragment that adds reachability and limited conjunction to DL-Lite while targeting NL data complexity through rewriting to nested two-way regular path queries.

read the letter

The main takeaway is that this work carves out ELbotpreceq as a Horn DL strictly between core DL-Lite and full ELI. It keeps data complexity in NL by stratifying how conjunction interacts with recursion and reachability axioms, then rewrites into nested two-way regular path queries that sit inside GQL-style languages. That directly addresses the AC0 versus PTime split that has limited OMQA to first-order rewritings so far, and it aligns with the NL-complete graph queries used in practice. The stratification move is the concrete new piece, and it looks like a sensible way to recover some expressivity without crossing into hardness. If the construction holds, it gives a usable fragment for graph-structured data that still extends DL-Lite in the intended directions. The soft spot is verification. The abstract states the NL upper bound and the rewriting target but does not spell out the stratification rules or the actual rewriting steps. Without those, it is not yet possible to confirm that every allowed combination stays inside NL and that no PTime-hard pattern (such as conjunctive transitive closure) slips through. The concern about whether stratification fully blocks the hard interactions is reasonable until the details are checked. This paper is for people working on OMQA, Horn DLs, and graph query languages who want something more than DL-Lite but still tractable. It shows clear thinking about the complexity landscape and engages the relevant literature without overclaiming. I would bring it to a reading group to walk through the stratification definition once the full text is available. It deserves peer review because the target result is well-motivated and the technical direction is coherent, even if revisions will be needed to supply the missing construction details.

Referee Report

2 major / 1 minor

Summary. The paper introduces ELbotpreceq, a stratified Horn extension of DL-Lite obtained from ELI by controlling the interaction between conjunction and recursion. It claims this logic strictly extends core DL-Lite while supporting reachability axioms and restricted conjunction, and establishes that ontology-mediated query answering has NL data complexity via a rewriting into nested two-way regular path queries (a fragment of GQL).

Significance. If the stratification and rewriting hold, the result is significant: it identifies a Horn DL whose data complexity sits strictly between the AC0 bound for DL-Lite and the PTime-hardness of most richer description logics, while targeting graph query languages whose complexity is NL-complete. The explicit rewriting target and the stratification construction are concrete strengths that could support practical OMQA extensions beyond first-order rewritability.

major comments (2)

[Abstract] Abstract: the NL upper bound is asserted via rewriting into nested two-way regular path queries, yet the abstract supplies neither the stratification definition nor the rewriting rules. Without these, it is impossible to verify that every permitted combination of restricted conjunction and reachability axioms remains inside NL and cannot encode a PTime-hard problem such as transitive closure over a conjunctive pattern.
[Stratification mechanism] Stratification mechanism: the central claim rests on the assertion that stratification blocks all PTime-hard interactions. The manuscript must supply either an explicit inductive argument or a representative set of allowed and disallowed axioms showing that no stratified ontology can still express a hard graph problem while remaining inside the permitted constructors.

minor comments (1)

[Introduction] The positioning of ELbotpreceq relative to existing Horn DLs would be clearer with a short comparison table listing expressivity and complexity for DL-Lite, EL, and the new logic.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback. We appreciate the recognition of the potential significance of ELbotpreceq as a Horn DL with NL data complexity. We respond to each major comment below and will incorporate revisions to strengthen the presentation.

read point-by-point responses

Referee: [Abstract] Abstract: the NL upper bound is asserted via rewriting into nested two-way regular path queries, yet the abstract supplies neither the stratification definition nor the rewriting rules. Without these, it is impossible to verify that every permitted combination of restricted conjunction and reachability axioms remains inside NL and cannot encode a PTime-hard problem such as transitive closure over a conjunctive pattern.

Authors: We agree that the abstract is high-level by design and omits the full technical definitions. The stratification is formally introduced and defined in Section 3, while the rewriting rules into nested two-way regular path queries (with the NL upper-bound proof) appear in Section 4. To address the concern, we will revise the abstract to include a concise description of the stratification mechanism and the rewriting target, making the key claims more self-contained without exceeding length limits. revision: yes
Referee: [Stratification mechanism] Stratification mechanism: the central claim rests on the assertion that stratification blocks all PTime-hard interactions. The manuscript must supply either an explicit inductive argument or a representative set of allowed and disallowed axioms showing that no stratified ontology can still express a hard graph problem while remaining inside the permitted constructors.

Authors: Section 3 defines the stratification on ELI ontologies to restrict conjunction-recursion interactions, and Section 4 proves the NL bound by exhibiting a semantics-preserving rewriting to nested 2RPQs. The rewriting itself serves as the argument that PTime-hard patterns (such as transitive closure over conjunctive queries) are excluded. To make this explicit, we will add (i) a short inductive argument in the proof of the main theorem showing that stratification prevents encoding of such patterns and (ii) a table of representative allowed and disallowed axiom combinations in Section 3. revision: yes

Circularity Check

0 steps flagged

No significant circularity: new stratification and rewriting are constructive definitions

full rationale

The paper defines a novel stratification mechanism on ELI to restrict conjunction-recursion interactions, yielding the new logic ELbotpreceq that extends DL-Lite while supporting reachability axioms. The NL upper bound is established by exhibiting an explicit rewriting into nested two-way regular path queries. No load-bearing step reduces to a fitted parameter, self-citation chain, or definitional tautology; the central claims rest on the fresh construction rather than renaming or importing prior author results as external facts. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central contribution is the new stratified logic itself; it relies on standard background results about description logic complexity and regular path queries rather than new free parameters or invented entities with independent evidence.

axioms (1)

standard math Standard complexity results for DL-Lite and regular path queries hold
Invoked to position the new NL bound against the existing AC0 vs PTime dichotomy.

invented entities (1)

ELbotpreceq no independent evidence
purpose: Stratified Horn extension of ELI/DL-Lite supporting reachability and restricted conjunction
Newly introduced logic whose properties are proved in the paper; no independent evidence outside the definition and rewriting.

pith-pipeline@v0.9.0 · 5529 in / 1216 out tokens · 41162 ms · 2026-05-14T18:45:33.108190+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

[1]

Calvanese, G

D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Tractable reasoning and efficient query answering in description logics: The DL-Lite family, Journal of Automated Reasoning (2007)

work page 2007
[2]

Calvanese, G

D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Data complexity of query answering in description logics, Artificial Intelligence (2013)

work page 2013
[3]

Libkin, W

L. Libkin, W. Martens, F. Murlak, L. Peterfreund, D. Vrgoc, Querying graph data: Where we are and where to go, in: PODS 2025, ACM, 2025

work page 2025
[4]

Francis, A

N. Francis, A. Gheerbrant, P. Guagliardo, L. Libkin, V. Marsault, W. Martens, F. Murlak, L. Peter- freund, A. Rogova, D. Vrgoc, A researcher’s digest of GQL (invited talk), in: ICDT 2023, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023

work page 2023
[5]

Bienvenu, M

M. Bienvenu, M. Ortiz, M. Šimkus, Regular path queries in lightweight description logics: Com- plexity and algorithms, Journal of Artificial Intelligence Research (2015)

work page 2015
[6]

Bienvenu, D

M. Bienvenu, D. Calvanese, M. Ortiz, M. Šimkus, Nested regular path queries in description logics, in: KR, 2014

work page 2014
[7]

Calvanese, T

D. Calvanese, T. Eiter, M. Ortiz, Regular path queries in expressive description logics with nominals, in: IJCAI 2009, 2009

work page 2009
[8]

Ortiz, S

M. Ortiz, S. Rudolph, M. Simkus, Query answering in the horn fragments of the description logics SHOIQ and SROIQ, in: T. Walsh (Ed.), IJCAI 2011, IJCAI/AAAI, 2011

work page 2011
[9]

Gheerbrant, L

A. Gheerbrant, L. Libkin, L. Peterfreund, A. Rogova, Database theory in action: Cypher, GQL, and regular path queries, in: ICDT 2025, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025

work page 2025
[10]

Francis, A

N. Francis, A. Gheerbrant, P. Guagliardo, L. Libkin, V. Marsault, W. Martens, F. Murlak, L. Peterfre- und, A. Rogova, D. Vrgoc, GPC: A pattern calculus for property graphs, in: PODS 2023, ACM, 2023

work page 2023
[11]

M. M. Dimartino, P. T. Wood, A. Calì, A. Poulovassilis, Efficient ontology-mediated query answering: Extending DL-LiteR and linear ELH, Journal of Artificial Intelligence Research (2025)

work page 2025
[12]

Löhnert, N

B. Löhnert, N. Augsten, C. Okulmus, M. Ortiz, Towards practicable algorithms for rewriting graph queries beyond DL-Lite, in: The Semantic Web, Springer Nature Switzerland, 2025

work page 2025
[13]

Dantsin, T

E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov, Complexity and expressive power of logic program- ming, ACM Computing Surveys (2001)

work page 2001
[14]

Baader, I

F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge Univer- sity Press, 2017

work page 2017
[15]

Ortiz, M

M. Ortiz, M. Šimkus, Reasoning and Query Answering in Description Logics, in: Reasoning Web, 2012

work page 2012
[16]

J. L. Reutter, M. Romero, M. Y. Vardi, Regular queries on graph databases, Theory Comput. Syst. 61 (2017)

work page 2017
[17]

T. J. Schaefer, The complexity of satisfiability problems, in: STOC, 1978

work page 1978
[18]

A. K. Chandra, D. Kozen, L. J. Stockmeyer, Alternation, Journal of the ACM (1981)

work page 1981
[19]

Baader, S

F. Baader, S. Borgwardt, M. Lippmann, Query rewriting for DL-Lite with n-ary concrete domains, in: IJCAI, 2017

work page 2017
[20]

Figueira, A

D. Figueira, A. Jeż, A. W. Lin, Data path queries over embedded graph databases, in: PODS 2022, 2022. A. Appendix on Soundness Here we provide the proof of Lemma 4.1, which we restate once more below. Lemma A.1.Let 𝒯 be a stratified ℰℒℐ ⊥ ⪯-TBox, A(𝑎) be an instance query, and AA be an nNFA from Definition 3.5. Then for all for all ABoxes𝒜we have that𝒜 |=...

work page 2022
[21]

To construct an accepting run of AA we can step from 𝑞0 := ({⊤},A) to 𝑞1 := ({⊤},⊤) , via a (sbus)-transition, which is already a final state

Suppose that A is a concept name and B =⊤ . To construct an accepting run of AA we can step from 𝑞0 := ({⊤},A) to 𝑞1 := ({⊤},⊤) , via a (sbus)-transition, which is already a final state. Then the sequence(a ℐ, 𝑞0,⊤?, 𝑞 1,a ℐ)is clearly a run ofA A starting froma ℐ

work page
[22]

Then, our derivation restricted to the first 𝑑−1 elements is a (𝒯, ℓ) -derivation of B(a) from 𝒜 of length 𝑑−1

Suppose A and B are concept names with B⪯A . Then, our derivation restricted to the first 𝑑−1 elements is a (𝒯, ℓ) -derivation of B(a) from 𝒜 of length 𝑑−1 . Hence, we can invoke the inductive hypothesis to obtain an accepting run 𝜌 := (a ℐ, 𝛿1,d 2), . . . ,(d𝑘−1, 𝛿𝑘,d 𝑘) of AB starting from aℐ. Note that this is also a run of A due to B⪯A . Applying the ...

work page
[23]

applied to

Suppose that A =⊥ or A is a concept name with B1 ⪯A and B2 ≺A , for concept names B1 and B2 where we have B = B 1 ⊓B 2 (the proof for B = B 2 ⊓B 1 is analogous). Then, our derivation restricted to the first 𝑑−1 elements is also a (𝒯, ℓ) -derivation of both B1(a) and B2(a) from 𝒜 of length 𝑑−1 . Hence, we can invoke the inductive hypothesis to obtain an ac...

work page