REVIEW 3 major objections 4 minor
Minimal Model Reasoning in Description Logics: Don't Try This at Home!
T0 review · 3 major / 4 minor · reviewed 2026-08-05 · deepseek-v4-flash
Pith's one-line read Pure minimal-model satisfiability is undecidable already for the description logic EL.
desk verdict Plausible and potentially significant negative results for EL and DL-Lite_horn, but abstract-only means the core reduction is unverifiable from this text. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the pure minimal model: a model in which the extension of every predicate is minimal under set inclusion, with no predicates left free to vary. The argument turns on a reduction that encodes an undecidable source problem into $\mathcal{EL}$ concept satisfiability, arranged so that the existence of a minimal model exactly mirrors a valid computation. The paper additionally uses acyclicity restrictions on the TBox as a structural condition that breaks the encoding and restores decidability; the connection to pointwise circumscription provides a bridge to existing complexity results.
What would settle it
The most direct way to test the claim is to inspect the announced reduction. A reader could look for an $\mathcal{EL}$ TBox and concept arising from the reduction where the concept is minimally satisfiable even though the encoded source instance is not a positive instance, or, conversely, a case where every model satisfying the encoding is automatically non-minimal, which would mean the reduction encodes an empty problem rather than the intended undecidable one.
Extended reading notes
Core claim
The paper establishes that checking whether a concept has a satisfiable pure minimal model—one in which the extension of every predicate is simultaneously minimal—is undecidable for the description logic $\mathcal{EL}$. In the same setting, it obtains ExpSpace-hardness for DL-Lite$_{\text{horn}}$, extending earlier positive decidability results known for DL-Lite$_{\text{core}}$. To regain decidability, the paper proposes acyclicity conditions on the TBox, bringing the worst-case complexity below double-exponential time and drawing a connection to pointwise circumscription. The undecidability also transfers to a very restricted fragment of tuple-generating dependencies.
Load-bearing premise
The load-bearing premise is that the reduction from an undecidable problem to $\mathcal{EL}$ minimal-model satisfiability faithfully encodes the source problem; if the encoding needs auxiliary predicates or constraints that $\mathcal{EL}$ cannot force to be minimal or fixed, the undecidability proof collapses.
Editorial extensions
If this is right
- For unrestricted $\mathcal{EL}$ TBoxes, there is no general algorithm that decides pure minimal-model concept satisfiability.
- The undecidability barrier is not an artifact of DL syntax, since it extends to a very restricted fragment of tuple-generating dependencies.
- Acyclicity conditions on the TBox yield decidable fragments with worst-case complexity below double-exponential time.
- DL-Lite$_{\text{horn}}$ minimal-model satisfiability is ExpSpace-hard, so the positive result for DL-Lite$_{\text{core}}$ does not extend to the Horn extension.
- The paper's data-complexity results complete the complexity picture for reasoning when only the data, not the ontology, varies.
Reading between the lines
- A practical consequence the authors leave implicit: any implemented reasoner for minimal-model semantics must either impose acyclicity, minimize only selected predicates as in circumscription, or settle for incomplete algorithms.
- The gap between decidable DL-Lite$_{\text{core}}$ and ExpSpace-hard DL-Lite$_{\text{horn}}$ suggests a sharp boundary; a natural next test is whether a single Horn axiom is enough to trigger the hardness.
- If pure minimality is undecidable in $\mathcal{EL}$, then ontology-mediated query answering under minimal-model semantics likely faces a similar barrier for queries that must inspect the minimal model itself.
- The acyclicity conditions that restore decidability may transfer to other lightweight DLs, but whether they are necessary rather than merely sufficient remains open.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies 'pure' minimal model reasoning in Description Logics, where the extensions of all predicates are required to be minimal. Based on the abstract, the main claims are: (1) concept satisfiability in minimal models is undecidable already for the lightweight DL EL; (2) undecidability extends to a very restricted fragment of tuple-generating dependencies; (3) acyclicity conditions on the TBox bring worst-case complexity below double exponential time and connect the setting to pointwise circumscription; (4) for DL-Lite_horn, minimal-model concept satisfiability is ExpSpace-hard, in contrast to a known positive result for DL-Lite_core. The abstract contains no formal definitions, theorem statements, or proof sketches; the full text was not available for review.
Significance. If the results are correct, they are significant. They would close a natural open direction for 'pure' minimal-model reasoning in a prominent lightweight DL, showing that this form of minimization is much harder than the underlying EL reasoning. The extension to TGDs and the DL-Lite_horn lower bound also map the boundary of tractability. The claimed connection to pointwise circumscription and the acyclicity conditions could provide a useful route to decidable fragments. The paper appears to be a pure theoretical contribution without empirical fitting, so there is no evident circularity. However, because the full text is unavailable, none of these claims can be verified from the submitted material.
major comments (3)
- [Abstract] The notion of minimal model is not defined. Key questions include: are all predicates minimized component-wise, and is the domain fixed or allowed to vary? Is the minimization pre-order inclusion on extensions? Most importantly, are minimal models guaranteed to exist for every satisfiable input? If the domain can vary, minimization may produce models with no minimal element, making 'satisfiable in a minimal model' ill-defined. These choices are load-bearing for the undecidability and hardness claims and must be specified in the full text.
- [Abstract] The central claim — undecidability of concept satisfiability in minimal models for EL — rests on a reduction that is not visible. A convincing proof must exhibit an encoding of an undecidable problem (e.g., tiling or Minsky machines) into an EL TBox and a concept such that satisfiability in a minimal model exactly encodes a valid computation. In particular, the encoding must rule out spurious infinite or cyclic models using only EL's limited expressivity (existential restrictions, conjunctions, no inverses/nominals/disjunction), and the minimality pre-order must select exactly the intended models. Without the construction, this claim cannot be assessed.
- [Abstract] The ExpSpace-hardness claim for DL-Lite_horn is presented as a second main result, but no proof strategy is given. Since DL-Lite_horn is closely tied to first-order rewritability, the lower bound likely relies on a careful encoding of an ExpSpace-hard problem into a DL-Lite_horn TBox and a minimal-model satisfiability query. The full paper must provide the reduction and its correctness proof; the abstract alone does not substantiate the claim.
minor comments (4)
- [Abstract] The phrase 'below double exponential time' is imprecise. Please state the exact complexity class (e.g., in 2-EXPTIME, or in co-N2EXP) and the matching lower bound, if applicable.
- [Abstract] The 'acyclicity conditions' on the TBox are not described. A short explanation or reference to the relevant definitions would help readers understand the scope of the decidability result.
- [Abstract] The 'data complexity' result is mentioned without a concrete statement. Please specify the complexity class and whether it applies to all the DLs considered.
- [Abstract] The connection to 'pointwise circumscription' is stated as a conclusion but not elaborated. A sentence describing the relationship would make the abstract more self-contained.
Circularity Check
No circularity found: the paper's claims are mathematical reduction results, not fitted or self-referential constructions.
full rationale
The available material is the abstract of a proof-based paper (arXiv:2508.05350). The central claims are that concept satisfiability in minimal models is undecidable for EL and ExpSpace-hard for DL-Lite_horn. These are theorem statements whose support would be a reduction from a known undecidable problem to EL minimal-model satisfiability, plus complexity arguments. Nothing in the abstract defines an output quantity in terms of the target result, fits parameters to a dataset and then calls the fit a prediction, or appeals to the authors' own prior work as the sole justification for a load-bearing premise. The abstract is self-contained with respect to circularity: it announces a negative complexity result and a route to decidability under acyclicity, both of which are standard mathematical claims that stand or fall with the proof, not with any circular definition. The skeptic's concern about the unverified reduction is a correctness/verifiability concern, not a circularity concern. Since no specific equation, definition, or self-citation can be exhibited as making the derivation equivalent to its inputs, the appropriate finding is no significant circularity.
Assumptions & free parameters
assumptions (2)
- standard math Standard undecidability result (e.g., tiling or halting problem) serves as the source for lower-bound reductions.
- domain assumption Description Logic semantics with minimal models: all predicate extensions are minimized simultaneously under set inclusion.
Cite this review
Pith. "Pith review of Minimal Model Reasoning in Description Logics: Don't Try This at Home!." pith.science (2026). https://pith.science/paper/F3D7IOVX
@misc{pith2026250805350,
author = {Pith},
title = {Pith review of: Minimal Model Reasoning in Description Logics: Don't Try This at Home!},
year = {2026},
howpublished = {\url{https://pith.science/paper/F3D7IOVX}},
note = {Machine review of arXiv:2508.05350}
}
abstract
Reasoning with minimal models has always been at the core of many knowledge representation techniques, but we still have only a limited understanding of this problem in Description Logics (DLs). Minimization of some selected predicates, letting the remaining predicates vary or be fixed, as proposed in circumscription, has been explored and exhibits high complexity. The case of `pure' minimal models, where the extension of all predicates must be minimal, has remained largely uncharted. We address this problem in popular DLs and obtain surprisingly negative results: concept satisfiability in minimal models is undecidable already for $\mathcal{EL}$. This undecidability also extends to a very restricted fragment of tuple-generating dependencies. To regain decidability, we impose acyclicity conditions on the TBox that bring the worst-case complexity below double exponential time and allow us to establish a connection with the recently studied pointwise circumscription; we also derive results in data complexity. We conclude with a brief excursion to the DL-Lite family, where a positive result was known for DL-Lite$_{\text{core}}$, but our investigation establishes ExpSpace-hardness already for its extension DL-Lite$_{\text{horn}}$.
Reviewed August 5, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.