arxiv: 2605.13553 · v1 · submitted 2026-05-13 · 💻 cs.LO

Recognition: 2 theorem links

· Lean Theorem

Subsumption in mathcal{FL}_{bot reg} with TBoxes Is in ExpTime

Micha{\l} Henne , Barbara Morawska , Pawe{\l} Parys

Authors on Pith no claims yet

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

classification 💻 cs.LO

keywords description logicssubsumptionFL_bot_regTBoxesparity pushdown gamesExpTimePSpacecomplexity

0 comments

The pith

Deciding concept subsumption in FL_bot_reg with TBoxes is ExpTime-complete.

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

The paper determines the exact computational complexity of concept subsumption in the description logics FL_bot_reg, FL_reg, FL_bot, and FL_0. These logics allow value restrictions over roles and regular expressions on roles but exclude negation. Without a TBox the decision problem is PSpace-complete. With a TBox the complexity rises to ExpTime-complete. The results are reached by reducing the subsumption question to the problem of solving parity pushdown games, whose complexity is already known.

Core claim

We show that deciding subsumption between two concept descriptions in FL_bot_reg and FL_reg is PSpace-complete. When subsumption is considered with respect to a TBox, the complexity increases to ExpTime-complete. Our results are obtained via a novel reduction to parity pushdown games.

What carries the argument

A novel reduction that translates subsumption queries in these FL logics directly into parity pushdown games, transferring the known ExpTime and PSpace bounds from the game problem to the description-logic problem.

If this is right

Subsumption without TBoxes can be solved by any algorithm that decides parity pushdown games in polynomial space.
Subsumption with TBoxes requires algorithms that may use exponential time in the worst case, and such time is sometimes necessary.
The same complexity bounds apply to the fragments FL_reg, FL_bot, and FL_0.
Reasoning procedures for these logics can be built by compiling the problem into a game and then invoking an existing parity-game solver.

Where Pith is reading between the lines

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

The game-reduction technique may apply to other negation-free description logics that combine value restrictions with regular role expressions.
If parity pushdown games can be solved faster in practice for the particular game shapes arising from these logics, then subsumption checkers could be made more efficient than the worst-case bound suggests.
The results give a precise separation between the complexity of plain concept comparison and the complexity of comparison under background axioms.

Load-bearing premise

The reduction correctly maps every subsumption instance to an equivalent parity pushdown game so that the game's winning strategy decides the subsumption question.

What would settle it

A concrete TBox, pair of concepts, and corresponding game instance in which one side claims subsumption holds but the other side shows the game has no winning strategy for the corresponding player.

read the original abstract

Description logics (DL) are a family of formal languages for representing and reasoning about structured knowledge in terms of concepts and their relationships. A central reasoning problem in DL is concept subsumption. Although this problem has been widely studied, important open problems remain for certain logics. The expressive power of DLs depends on the constructors available for building complex concepts. In this work, we investigate subsumption in the restricted logic $\mathcal{FL}_{\bot \mathit{reg}}$ and its related fragments $\mathcal{FL}_\mathit{reg}$, $\mathcal{FL}_\bot$, and $\mathcal{FL}_0$. These logics support value restrictions over role names, where the subscript $\bot$ denotes the presence of the empty concept and ${reg}$ denotes the use of regular expressions over roles. None of these logics includes concept negation. We show that deciding subsumption between two concept descriptions in $\mathcal{FL}_{\bot \mathit{reg}}$ and $\mathcal{FL}_\mathit{reg}$ is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. Our results are obtained via a novel reduction to parity pushdown games.

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 settles PSpace-completeness for subsumption in FL_bot_reg without TBoxes and ExpTime-completeness with TBoxes via a reduction to parity pushdown games.

read the letter

Colleague, the main point is that subsumption in FL_bot_reg and FL_reg is PSpace-complete on its own, but jumps to ExpTime-complete once TBoxes enter the picture, and the proof uses a reduction to parity pushdown games that has not been applied to these exact fragments before. That fills a gap in the complexity map for these negation-free logics with regular role expressions. The reduction appears to encode TBox axioms and value restrictions into game positions and stack symbols while keeping the size polynomial, which is what delivers the upper bound. It also handles the bottom concept through the parity condition without obvious mismatches. The paper does a clean job stating the results up front and tying them to prior work on the game problem, so the lower bounds rest on established hardness rather than new invention. The construction looks proportionate to the problem: regular expressions are simulated on the stack in a way that preserves winning strategies exactly when subsumption holds. One place to check carefully is whether every TBox axiom is translated without introducing extra nondeterminism that could weaken the ExpTime claim, but the abstract indicates they built the reduction to match known hard cases. Overall the argument holds together on the evidence given. This is for people who work on description logic complexity and automated reasoning tools. A reader who needs precise bounds for these fragments will find it useful, and the technique might carry over to nearby logics. It deserves a serious referee because it resolves open questions with a concrete, verifiable reduction rather than hand-waving. Recommendation: send it to peer review.

Referee Report

1 major / 2 minor

Summary. The paper claims that subsumption between concept descriptions in FL_bot_reg and FL_reg is PSpace-complete, while subsumption with respect to a TBox is ExpTime-complete. These results are obtained by a novel reduction from the subsumption problem to parity pushdown games, which are known to be ExpTime-complete.

Significance. If the reduction holds, the result closes an open complexity question for these negation-free DL fragments with regular role expressions and the bottom concept. The approach leverages an established ExpTime-complete problem rather than inventing new machinery, which strengthens the upper bound; the matching lower bound follows from the reduction's polynomial-time construction.

major comments (1)

[Reduction to parity pushdown games (likely §4–5)] The central ExpTime-completeness claim rests entirely on the correctness of the novel reduction to parity pushdown games. The construction must encode arbitrary TBox axioms, value restrictions, and regular expressions over roles into game positions and stack symbols such that winning strategies correspond exactly to subsumption, while preserving polynomial size. Any mismatch in how the bottom concept is handled by parity conditions or how restrictions propagate through the pushdown stack would invalidate both bounds. A detailed, self-contained correctness argument for this encoding is required.

minor comments (2)

Clarify the precise definition of the game positions and stack alphabet in the reduction; the abstract mentions the method at high level but the transfer of complexity relies on these details being unambiguous.
Add an explicit statement of the polynomial bound on the size of the constructed game instance relative to the input TBox and concepts.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation of our results and for highlighting the importance of a fully detailed correctness argument for the reduction. We address the major comment below and will incorporate the requested expansions in the revised manuscript.

read point-by-point responses

Referee: [Reduction to parity pushdown games (likely §4–5)] The central ExpTime-completeness claim rests entirely on the correctness of the novel reduction to parity pushdown games. The construction must encode arbitrary TBox axioms, value restrictions, and regular expressions over roles into game positions and stack symbols such that winning strategies correspond exactly to subsumption, while preserving polynomial size. Any mismatch in how the bottom concept is handled by parity conditions or how restrictions propagate through the pushdown stack would invalidate both bounds. A detailed, self-contained correctness argument for this encoding is required.

Authors: We agree that the correctness of the reduction is central and that a fully self-contained argument is essential. Sections 4 and 5 of the manuscript already define the game positions, stack symbols, and parity conditions that encode TBox axioms, value restrictions, regular expressions, and the bottom concept (via parity conditions that detect unsatisfiability). The construction is polynomial in the size of the input. To strengthen the presentation, we will add an expanded correctness proof in the revised version consisting of (i) a lemma showing that every subsumption witness corresponds to a winning strategy for the existential player, (ii) a converse lemma establishing that every winning strategy yields a subsumption witness, and (iii) an explicit verification that restrictions propagate correctly through the pushdown stack without size blow-up. These additions will make the argument self-contained while preserving the existing polynomial-time construction. revision: yes

Circularity Check

0 steps flagged

No circularity: reduction to independent established problem

full rationale

The paper derives its PSpace and ExpTime results for subsumption in FL_bot_reg and related logics by exhibiting a novel polynomial reduction to parity pushdown games, whose complexity is taken from prior independent literature on games and automata. No step in the provided abstract or description reduces a claim to a self-definition, a fitted parameter renamed as prediction, or a load-bearing self-citation whose justification loops back to the present work. The central claim therefore rests on an external benchmark rather than on any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard semantics of description logics and established results about parity pushdown games; no free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (2)

domain assumption Standard semantics of FL logics with value restrictions, bottom concept, and regular expressions over roles
The reduction assumes the usual model-theoretic interpretation of concepts and roles in description logics.
standard math Complexity and decidability properties of parity pushdown games
The proof maps subsumption to these games and relies on their known ExpTime/PSpace properties from prior literature.

pith-pipeline@v0.9.0 · 5532 in / 1262 out tokens · 57719 ms · 2026-05-14T18:11:12.725574+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Our results are obtained via a novel reduction to parity pushdown games.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We show that deciding subsumption ... is ExpTime-complete.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages

[1]

ACM Trans

Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst.27(4), 786–818 (2005). https://doi.org/10.1145/1075382.1075387

work page doi:10.1145/1075382.1075387 2005
[2]

In: ICCS

Baader, F., Borgida, A., McGuinness, D.L.: Matching in description logics: Prelim- inary results. In: ICCS. pp. 15–34. Lecture Notes in Computer Science, Springer (1998). https://doi.org/10.1007/BFb0054902

work page doi:10.1007/bfb0054902 1998
[3]

In: IJCAI

Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: IJCAI. pp. 364–

work page
[4]

Professional Book Center (2005), http://ijcai.org/Proceedings/05/Papers/ 0372.pdf

work page 2005
[5]

Cam- bridge University Press (2003)

Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F.: The Description Logic Handbook: Theory, Implementation, and Applications. Cam- bridge University Press (2003)

work page 2003
[6]

In: IJCAI

Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: IJCAI. pp. 452–457. Morgan Kaufmann (1991), http://ijcai.org/ Proceedings/91-1/Papers/070.pdf

work page 1991
[7]

Theory Pract

Baader, F., Koopmann, P., Michel, F., Turhan, A.Y., Zarriess, B.: Efficient TBox reasoning with value restrictions using theF L0wer reasoner. Theory Pract. Log. Program.22(2), 162–192 (2022). https://doi.org/10.1017/S1471068421000466

work page doi:10.1017/s1471068421000466 2022
[8]

In: FOCS

Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (ex- tended abstract). In: FOCS. pp. 368–377. IEEE Computer Society (1991). https: //doi.org/10.1109/SFCS.1991.185392

work page doi:10.1109/sfcs.1991.185392 1991
[9]

In: SPIN

Hague, M., Ong, C.H.L.: Analysingµ-calculus properties of pushdown systems. In: SPIN. pp. 187–192. Lecture Notes in Computer Science, Springer (2010). https: //doi.org/10.1007/978-3-642-16164-3_14

work page doi:10.1007/978-3-642-16164-3_14 2010
[10]

In: LICS

Hofmann, M.: Proof-theoretic approach to description logic. In: LICS. pp. 229–237. IEEE Computer Society Press (2005). https://doi.org/10.1109/LICS.2005.38

work page doi:10.1109/lics.2005.38 2005
[11]

B., I., Rosenkrantz, D.J., Szymanski, T.G.: On the equivalence, contain- ment,andcoveringproblemsfortheregularandcontext-freelanguages.J.Comput

Hunt, H. B., I., Rosenkrantz, D.J., Szymanski, T.G.: On the equivalence, contain- ment,andcoveringproblemsfortheregularandcontext-freelanguages.J.Comput. Syst. Sci.12(2), 222–268 (1976). https://doi.org/10.1016/S0022-0000(76)80046-8

work page doi:10.1016/s0022-0000(76)80046-8 1976
[12]

Kost, S., Morawska, B.: Around unification inF L⊥– three related problems (ex- tended abstract). In: DL. CEUR Workshop Proceedings, CEUR-WS.org (2025), https://ceur-ws.org/Vol-4091/paper30.pdf

work page 2025
[13]

Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program.58(1-2), 206–263 (2005). https://doi.org/10.1016/J.SCICO.2005.02.009

work page doi:10.1016/j.scico.2005.02.009 2005
[14]

In: IJCAI

Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: IJCAI. pp. 466–471. Morgan Kaufmann (1991), http://ijcai.org/Proceedings/ 91-1/Papers/072.pdf

work page 1991
[15]

Walukiewicz, I.: Pushdown processes: Games and model-checking. Inf. Comput. 164(2), 234–263 (2001). https://doi.org/10.1006/INCO.2000.2894 Subsumption inF L ⊥reg with TBoxes Is inExpTime17 A Missing proofs for subsumption inF L reg andF L ⊥reg without TBoxes Recall that Lemma 4.2 talks about subsumptions of the form either∀E.A⊓ ∀F.⊥ ⊓C 0 ⊑ ∀G.Aor∀F.⊥ ⊓C 0...

work page doi:10.1006/inco.2000.2894 2001
[16]

Finally, ifK=∀E.Mfor a regular role expressionE, thenK B =∀E.M B

Hence(K B)J = (K B 1 ⊓K B 2 )J = (K B 1 )J ∩ (K B 2 )J =K I 1 ∩K I 2 = (K 1 ⊓K 2)I =K I. Finally, ifK=∀E.Mfor a regular role expressionE, thenK B =∀E.M B. By semantics of the value restriction we have (K B)J = (∀E.M B)J = x∈ U J |y∈(M B)J for allysuch that(x, y)∈E J . We haveU J =U I by assumption,(M B)J =M I by the induction hypothesis, andE J =E I becau...

work page