arxiv: 2604.25549 · v1 · submitted 2026-04-28 · 💻 cs.LO

Recognition: unknown

Partially Finite Model Reasoning in Description Logics Extended Version

Alexandra Rogova, Filip Murlak, Marcin Przyby{\l}ko, Micha{\l} Skrzypczak, Tomasz Gogacz

Authors on Pith no claims yet

Pith reviewed 2026-05-07 14:26 UTC · model grok-4.3

classification 💻 cs.LO

keywords description logicspartially finite modelsconjunctive query entailment2-EXPTIMEmodel surgeryclosed predicatesDL Sfinite model reasoning

0 comments

The pith

Partially finite entailment of conjunctive queries in description logic S is in 2-EXPTIME.

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

The paper introduces partially finite models, where a distinguished concept must be interpreted as a finite set while the rest of the model may be infinite. It examines the decision problem of whether a conjunctive query holds in all such models of a knowledge base in the description logic S. The authors establish that this partially finite query entailment problem lies in 2-EXPTIME. The result unifies prior work on purely finite and purely infinite cases through a new proof technique and directly enables reduction of query containment under closed predicates to this setting.

Core claim

We initiate the study of partially finite models for harmonising finite and infinite model reasoning. For the description logic S we show that partially finite entailment of conjunctive queries is in 2-EXPTIME. The solution involves sophisticated infinite model surgery and goes far beyond combining the arguments for the two special cases. As a direct application, the problem of query containment in the presence of closed predicates can be solved by reduction to partially finite query entailment.

What carries the argument

Sophisticated infinite model surgery that enforces finiteness only on a distinguished concept while preserving entailment properties for conjunctive queries.

If this is right

Query containment in the presence of closed predicates reduces directly to partially finite query entailment.
Finite and infinite reasoning modes in S can be treated uniformly without separate algorithms.
The 2-EXPTIME bound holds even when the model mixes finite and infinite interpretations under the partial constraint.
Prior techniques for finite and infinite entailment combine into a single procedure that does not raise complexity.

Where Pith is reading between the lines

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

The model surgery approach may extend to other description logics where finite and infinite entailment already diverge in complexity.
Reasoning engines could implement partial finiteness to support hybrid knowledge bases that mix closed and open predicates.
Similar surgery constructions might control finiteness constraints in related modal or temporal logics without complexity blowup.

Load-bearing premise

The infinite model surgery technique can be generalized from the pure finite and pure infinite cases to the partially finite setting without introducing new sources of undecidability or higher complexity.

What would settle it

A knowledge base, query, and distinguished concept in S where deciding partially finite entailment requires more than 2-EXPTIME time or becomes undecidable would falsify the central claim.

Figures

Figures reproduced from arXiv: 2604.25549 by Alexandra Rogova, Filip Murlak, Marcin Przyby{\l}ko, Micha{\l} Skrzypczak, Tomasz Gogacz.

**Figure 1.** Figure 1: Unrestricted and partially finite interpretations. view at source ↗

**Figure 2.** Figure 2: An interpretation and its quasi-unravelling. view at source ↗

**Figure 3.** Figure 3: The three levels of elementary interpretations. Critical elements indicated with concept name view at source ↗

**Figure 4.** Figure 4: An illustration to the proof of Theorem 10. view at source ↗

**Figure 5.** Figure 5: Overview of the constructions used in proofs of Sec view at source ↗

**Figure 6.** Figure 6: In relation to the diagram of Figure 5 it is a more view at source ↗

**Figure 6.** Figure 6: Overview of the proof strategy for Theorem 11. view at source ↗

**Figure 7.** Figure 7: The proof overview for Lemma 12. Dashed arrows show view at source ↗

read the original abstract

Aiming to harmonise finite and infinite model reasoning, we initiate the study of partially finite models, where the reasoning task comes with a formula that specifies a part of the model that must be finite. We focus on the problem of partially finite query entailment in description logics (DLs): given a knowledge base (KB), a query, and a distinguished concept, decide whether the query holds in all models of the KB that interpret the distinguished concept as a finite set. To break the ground, we work with the DL S, an extension of the basic DL ALC with transitive roles, which is one of the simplest cases where finite and infinite query entailment diverge. Generalising previous results on the finite and infinite cases, we show that also partially finite entailment of conjunctive queries is in 2-exptime for S. The solution involves sophisticated infinite model surgery and goes far beyond combining the arguments for the two special cases. As a direct application, we show how the problem of query containment in the presence of closed predicates can be solved by reduction to partially finite query entailment.

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 introduces partially finite query entailment and claims a 2-EXPTIME bound for S via model surgery that goes beyond combining finite and infinite cases, plus a reduction for closed-predicate containment.

read the letter

The one or two things to know: this paper starts the study of partially finite models in description logics and establishes that partially finite conjunctive query entailment for S is in 2-EXPTIME. The approach uses infinite model surgery that they describe as more involved than just gluing the finite and infinite cases together. As a bonus, it reduces query containment with closed predicates to this problem. They do a good job laying out why partial finiteness is a useful intermediate notion, especially for knowledge bases that have some finite components but not all. The reduction to the closed predicate problem is clean and shows immediate relevance. The potential weak point is in the complexity proof. The stress test flags that generalizing the surgery to handle a distinguished finite concept alongside transitive roles might not stay within 2-EXPTIME if there are unaccounted interactions, like role chains crossing the boundary. The paper says the technique is sophisticated, so presumably they have a way to manage it without extra exponential blowup or undecidability, but that part needs careful reading to confirm no new sources of hardness creep in. Overall, this is for specialists in DL complexity and finite model reasoning. A reader who follows work on ALC with transitive roles or query entailment will get something from the new definitions and the application, even if they don't buy the full proof yet. It is worth a serious referee because it introduces a fresh problem with a claimed tight complexity bound and a practical hook. The math seems grounded in prior results by the same group. Recommendation: Yes, send it to peer review. Ask the referees to focus on whether the model surgery truly preserves the 2-EXPTIME bound without additional costs from the partial constraints.

Referee Report

0 major / 2 minor

Summary. The paper introduces the concept of partially finite models in description logics, where a distinguished concept must be interpreted as a finite set. Focusing on the DL S (ALC extended with transitive roles), it proves that entailment of conjunctive queries under partially finite semantics is in 2-EXPTIME. The proof relies on a sophisticated generalization of infinite model surgery that extends prior techniques for purely finite and purely infinite cases. As an application, it reduces query containment in the presence of closed predicates to this entailment problem.

Significance. If the central result holds, the work provides a unified 2-EXPTIME bound for a new reasoning task that interpolates between finite and infinite model reasoning in DLs, which is relevant for applications such as query containment with closed-world assumptions. Credit is due for the non-trivial model surgery construction that preserves the complexity bound despite the interactions between finite and infinite model parts.

minor comments (2)

[Abstract] The abstract refers to 'sophisticated infinite model surgery' without a one-sentence high-level outline of the key new idea; adding this would improve accessibility.
[Section 4] Some notation for the distinguished concept and the partial finiteness constraint could be introduced earlier and used consistently in the complexity proof.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, recognition of the significance of unifying finite and infinite model reasoning via partially finite models, and the recommendation for minor revision. The report does not raise any specific major comments.

Circularity Check

0 steps flagged

No circularity: complexity bound derived via explicit model-theoretic construction

full rationale

The paper establishes the 2-EXPTIME upper bound for partially finite conjunctive query entailment in DL S through a direct generalization of prior finite and infinite model results, using an explicit infinite model surgery technique. This construction is described as going 'far beyond combining the arguments for the two special cases' and is presented as a self-contained model-theoretic argument rather than a reduction to fitted parameters, self-definitions, or load-bearing unverified self-citations. No equations or steps in the abstract reduce the claimed result to its inputs by construction; the derivation remains independent and externally falsifiable via the provided model surgery.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard mathematical axioms for complexity classes and model theory. No free parameters or invented entities beyond the new definition of partially finite models are introduced.

axioms (1)

standard math Standard assumptions of complexity theory (closure properties of 2-EXPTIME under reductions and model constructions).
Invoked implicitly when claiming membership in 2-EXPTIME.

invented entities (1)

Partially finite model no independent evidence
purpose: Model that interprets a distinguished concept as finite while allowing the rest to be infinite.
This is the core new concept defined to harmonize finite and infinite reasoning.

pith-pipeline@v0.9.0 · 5504 in / 1331 out tokens · 61265 ms · 2026-05-07T14:26:32.906409+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 1 canonical work pages · 1 internal anchor

[1]

ijcai.org, 2019. Piero A. Bonatti, Carsten Lutz, and Frank Wolter. The complexity of circumscription in dls.J. Artif. Intell. Res., 35:717–773, 2009. Andrea Cal`ı, Georg Gottlob, and Thomas Lukasiewicz. Dat- alog extensions for tractable query answering over ontolo- gies. In Roberto De Virgilio, Fausto Giunchiglia, and Letizia Tanca, editors,Semantic Web ...

work page internal anchor Pith review arXiv 2019
[2]

The setP s has at most|P|−selements
[3]

Each piece inP s is connected as a graph
[4]

IfQ ′,Q ′′ ∈P s are distinct pieces then they do not share non-coloured elements
[5]

The union SPs treated as an interpretation equalsQ(tak- ing into account domain, concepts, and roles)
[6]

For each pieceQ ′ ∈P s there exists a coloured homomor- phismh Q′ :Q ′ → I
[7]

Ifθ(f 1) = θ(f 2)thenh Q1(f 1)andh Q2(f 2)are∼ k·(|P|−s)-equivalent

Considerf 1,f 2 ∈Dthat are two coloured elements such thatf 1 ∈∆ Q1 andf 2 ∈∆ Q2 withQ 1,Q 2 ∈P s. Ifθ(f 1) = θ(f 2)thenh Q1(f 1)andh Q2(f 2)are∼ k·(|P|−s)-equivalent. All the conditions except the last one simply express how the piecesP s splitQ. The last condition is crucial: it pre- serves the ability to glue pieces whenever they share ele- ments of th...
[8]

Since for i=1,2 holds that[f ′ i ]∼K =h(f i), the unary types off ′ i and h(f i)agree

This map clearly defines the desired homomorphism. Since for i=1,2 holds that[f ′ i ]∼K =h(f i), the unary types off ′ i and h(f i)agree. Preservation of rolerfollows directly form the construction. For any other role namessuch that(f 1,f 2)∈ sQ, sincehis a homomorphism, there aref ′′ 1 andf ′′ 2 such that(f ′′ 1 ,f ′′ 2 )∈s I and are∼ K equivalent respec...
[9]

Note thatκ(f ′

Thus, by∼ 1 equivalence off ′ 1 andf ′′ 1 (K≥1), we know that there isf ′′′ 2 which is connected by ansedge tof ′ 1. Note thatκ(f ′
[10]

It remains to see thatf ′′′ 2 =f ′ 2, but this follows directly from the fact that IisK-sparse andK>0

=κ(f ′′ 2 ) =κ(f ′′′ 2 ) =θ(f 2). It remains to see thatf ′′′ 2 =f ′ 2, but this follows directly from the fact that IisK-sparse andK>0. What remains is to define the homomorphism for pieces of the formQ e for non-coloured elementse∈E. Here the domain isD(e)∪E(e). The parth↾E(e)is already a proper homomorphismh ′ ofQ↾E(e)intoIbecause there is no ambiguity...
[11]

We assume thatθ(f ′

Thus, considerf ′ 1 ∈dom(h ′ 1)which is a coloured element, any pieceQ ′ ∈P s+1, and anyf ′ 2 ∈∆ Q′ which is also coloured. We assume thatθ(f ′
[12]

First note two obvious consequences of the definition of k-equivalence

=θ(f ′ 2)and we need to show thaty 2 def=h ′ 1(f ′ 1)andy ′ 2 def=h Q′(f ′ 2)are∼ k·(|P|−s−1) equivalent. First note two obvious consequences of the definition of k-equivalence. Fact 19.For k≥k ′ ≥0, if x∼ k y then also x∼ k′ y. Fact 20.If h:I → Jis a homomorphism and x,y∈∆ I then dJ (h(x),h(y))≤d I(x,y). Observe thaty 1 def=h 1(f ′ 1)is∼ k·(|P|−s) equiva...
[13]

Theorem 10

=h ′(y1); •x 1 =f 1 =h 1(f),x 2 =f 2 =h 2(f) =h ′ 1(f); Thus, we know thatK≥kbecause|P| ≤2·k 2. Clearlyk≥ jandj≥0 becausek>0 and|P|−s≥2. Moreover,x 1 ∼k x2 due to the inductive assumption abouth 1 andh 2. The parameters are so thatk−j=k, so we know thatd(y 1,x 1)≤ kandd(y 2,x 2)≤k. Merging homomorphisms.LetF=F I be the set of coloured elements inI. First ...

1927