Pith Number

pith:MKLTKVJL

pith:2026:MKLTKVJLQHH4ZTOODN2SERRGQB

not attested not anchored not stored refs resolved

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

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

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

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

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{MKLTKVJLQHH4ZTOODN2SERRGQB}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest 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.

C2weakest assumption

That the novel reduction to parity pushdown games correctly captures the subsumption problem and that the complexity of the game problem transfers appropriately to the DL setting.

C3one line summary

Subsumption in FL_bot_reg and FL_reg is PSpace-complete without TBoxes and ExpTime-complete with TBoxes via reduction to parity pushdown games.

References

16 extracted · 16 resolved · 0 Pith anchors

[1] 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/107 2005 · doi:10.1145/1075382.1075387

[2] 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/BFb00 1998 · doi:10.1007/bfb0054902

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

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

[5] Cam- bridge University Press (2003) 2003

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-18T02:44:23.704102Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

629735552b81cfcccdce1b75224626805abcd12b87ebbff3c899976cf4366d77

Aliases

arxiv: 2605.13553 · arxiv_version: 2605.13553v1 · doi: 10.48550/arxiv.2605.13553 · pith_short_12: MKLTKVJLQHH4 · pith_short_16: MKLTKVJLQHH4ZTOO · pith_short_8: MKLTKVJL

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/MKLTKVJLQHH4ZTOODN2SERRGQB \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 629735552b81cfcccdce1b75224626805abcd12b87ebbff3c899976cf4366d77

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "f41006edea56a97d38ca0159c66049738b017c08988f7db1a9c3a41a4afd58be",
    "cross_cats_sorted": [],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-13T13:57:31Z",
    "title_canon_sha256": "521ab7a130d487ad27f3419523465923407970841d12d1585df54ad876e4ed90"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.13553",
    "kind": "arxiv",
    "version": 1
  }
}