Pith. sign in

REVIEW 1 major objections 3 minor 33 references

Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)

T0 review · 1 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper proves that a logic combining expressive cardinality constraints on role successors with concrete-domain feature comparisons, nominals, and feature roles has the same consistency complexity as basic ALC: ExpTime-complete for…

desk verdict Strong paper with a fixable gap in Lemma 2's successor indexing; the core ExpTime-completeness theorem is likely correct. read the letter →

arxiv 2505.21103 v1 pith:PSEXSHQ6 submitted 2025-05-27 cs.LO

Franz Baader , Stefan Borgwardt , Filippo De Bortoli , Patrick Koopmann This is my paper
classification cs.LO MSC 68Q1768Q2568T27
keywords descriptionlogicsconcretedomainscardinalityconstraintsQFBAPAomega-admissibleExpTime-completenessundecidabilitytypeelimination
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Description logics are knowledge-representation languages in which concept inclusions say how sets of individuals relate, and quantitative information normally enters through either counting role successors or comparing values of concrete features such as salaries. This paper studies the logic $\mathcal{ALCOSCC}(\mathfrak{D})$, which allows both at once: succ-restrictions built from QFBAPA set and cardinality constraints can count role successors that satisfy arbitrary Boolean combinations of roles, concepts, and feature roles, while concrete domain restrictions can compare feature values along feature paths. The paper's central claim is that, whenever the concrete domain $\mathfrak{D}$ is ExpTime-$\omega$-admissible and its constraint satisfaction problem lies in ExpTime, consistency of TBoxes in this logic is ExpTime-complete, the same complexity as basic $\mathcal{ALC}$. The significance is that the two quantitative mechanisms can be combined, with nominals and feature roles, without crossing a complexity threshold. The paper also shows the combination is fragile: mixing feature values directly into cardinality expressions, allowing global cardinality restrictions, or adding transitive roles makes consistency undecidable for natural domains.

What carries the argument

The load-bearing object is the augmented type $(t,V,\mathcal{C}_t)$: a description-logic type $t$ (a maximal consistent set of subconcepts and their negations), a Venn bag $V$ recording how many role successors of each Venn region the type promises to realise, and a complete constraint system $\mathcal{C}_t$ over feature variables fixing all concrete values relevant to $t$ and $V$. The QFBAPA formula $\phi_t$ turns the counting part of a type into a set and cardinality constraint, and Lemma 1 from [3] guarantees a polynomial bound on the number of non-empty Venn regions needed, so bags stay small. Algorithm 1 guesses an individual type system, named augmented types, and anonymous augmented types, then eliminates any type not patched by a successor augmented type; the patch condition demands that the successor type's concept memberships contain the Venn region's requirements and that the merged constraint systems remain satisfiable. Patchwork and homomorphism $\omega$-compactness lift the finite amalgamation steps to a full model, and the exponential bound comes from the fact that only exponentially many augmented types exist.

What would settle it

To falsify the ExpTime upper bound, one would exhibit an ExpTime-$\omega$-admissible concrete domain $\mathfrak{D}$ and a sequence of $\mathcal{ALCOSCC}(\mathfrak{D})$ TBoxes whose consistency check forces the type-elimination algorithm to consider more than exponentially many augmented types, or forces the QFBAPA formula in some type to be satisfiable only with more than polynomially many non-empty Venn regions. Since Lemma 1 is the step that bounds Venn bags, a counterexample QFBAPA formula satisfying the conditions of that lemma but needing exponentially many non-empty Venn regions in every solution would directly break the construction.

Watch

Extended reading notes

Core claim

Let $\mathfrak{D}$ be a relational structure over a finite signature that is a patchwork (its predicates partition each arity, equality is first-order definable, and satisfiable constraint systems agreeing on shared variables can be amalgamated), is homomorphism $\omega$-compact (a countable constraint system is satisfiable as soon as all finite subsystems are), and has a constraint satisfaction problem decidable in exponential time. Under these assumptions the paper proves that consistency checking in $\mathcal{ALCOSCC}(\mathfrak{D})$ is ExpTime-complete. The upper bound is obtained by a type-elimination algorithm whose states are augmented types, each carrying a QFBAPA Venn bag for role successors and a complete concrete constraint system for feature values. The lower bound is inherited from $\mathcal{ALC}$. Theorem 1 establishes that feature roles genuinely increase expressivity, and Theorem 3 extends the result to ABox feature assertions for homogeneous ExpTime-$\omega$-admissible domains with constants.

Load-bearing premise

The result depends on the concrete domain $\mathfrak{D}$ satisfying every condition of Definition 1—finite signature, patchwork, homomorphism $\omega$-compactness, and an ExpTime constraint satisfaction problem—and if an application domain fails one of these, the exponential-time construction does not apply and known examples make the logic undecidable.

Editorial extensions

If this is right

  • For any ExpTime-$\omega$-admissible $\mathfrak{D}$, such as the rational order $(\mathbb{Q},<,=,>)$, Allen's interval algebra, or RCC8 under the stated conditions, consistency in $\mathcal{ALCOSCC}(\mathfrak{D})$ is ExpTime-complete, so sophisticated counting and concrete value comparisons are available at the same asymptotic cost as plain ALC.
  • Feature roles allow the concrete values of role successors to enter counting constraints, enabling statements such as 'earns less than the majority of their children' that cannot be expressed by concrete-domain restrictions alone.
  • For homogeneous ExpTime-$\omega$-admissible domains with constants, feature assertions and singleton predicates can be added to the ABox without increasing complexity.
  • The undecidability results delimit the reach of the method: mixed numerical constraints $f=\ell$, global sat-restrictions, and transitive roles each make consistency undecidable, so the ExpTime bound sits at a sharp design boundary.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A practical reasoner for the logic could be assembled by connecting a QFBAPA solver to a concrete-domain consistency checker through the Venn-bag interface; the paper mentions implementation as future work, but the elimination algorithm already fixes the exponential search structure.
  • The undecidability proofs encode multiplication of cardinalities and tiling, which suggests that permitting arithmetic inside the concrete domain itself, rather than only comparing feature values, is likely to be undecidable even for very simple domains; the paper's mixed-constraint result already gives one point on that slope.
  • The complexity of $\mathcal{ALCOISCC}(\mathfrak{D})$ with full inverse roles is left open; based on how inverse roles raise the complexity of classical DLs with nominals and number restrictions to NExpTime, a natural conjecture is that the inverse-role extension jumps to NExpTime as well.
  • A consequence the authors leave implicit is that every newly discovered concrete domain satisfying Definition 1 automatically inherits the same ExpTime bound, giving a cheap test for extending the result to other spatial or temporal formalisms whose CSP is in ExpTime.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 3 minor

Summary. The paper introduces the description logic ALCOSCC(D), which combines the QFBAPA-based cardinality constraints on role successors from ALCSCC with ω-admissible concrete domains, feature paths, feature roles, and nominals. The central result (Theorem 2) is that consistency checking in ALCOSCC(D) is ExpTime-complete whenever CSP(D) is in ExpTime, matching the complexity of plain ALC. The paper also treats ABox extensions via feature and predicate assertions (Section 5, Lemmas 4–5, Theorem 3) and establishes undecidability for several apparently mild extensions, including mixed value/cardinality constraints, global sat-restrictions, and transitive roles (Section 6). The proof uses a type-elimination algorithm; all details are in the appendix.

Significance. If the main theorem holds, it identifies a remarkably expressive DL whose consistency problem has the same worst-case complexity as ALC, under a generic model-theoretic condition on the concrete domain. The accompanying undecidability results delimit the boundary of this tractability and are a useful contribution in themselves. The paper is careful about stating its external dependencies (QFBAPA, ω-admissible concrete domains, ExpTime-hardness of ALC), and the extended version contains detailed appendix proofs and explicit reductions. The one load-bearing gap I found is local and appears repairable, so the overall contribution is potentially publishable after revision.

major comments (1)
  1. [§4, Lemma 2 and Appendix A.1, Lemma 6] The model construction in the soundness direction is not well-defined as written. Lemma 2 first selects, for each v∈supp(V) and each 1≤i≤V(v), an augmented type t(v,i) that patches t at (v,i). The definition of Δ_{m+1}^r[a,w] then creates successors (a, w·(t(v,i), v, j)) with i = max(j,V(v)). For j>V(v) this refers to t(v,j), which has not been introduced, and for 1≤j<V(v) it uses t(v,V(v)), which is only known to patch at (v,V(v)), not at (v,j). This matters because Definition 5 gives the local system separate feature variables f^{(v,j)} for each 1≤j≤V(v), and Definition 6 requires a patch at (v,j) to constrain those variables. Consequently, Lemma 6's claim that t patches end(a,w') at (v,i) does not yield agreement on the variables f^{(v,1)},...,f^{(v,V(v)-1)}, and the proof does not establish that the merged infinite constraint system is satisfiable. The natural correction is to set i = min(j,V(v)): use t(v,j) for the j-th required successor when j≤V(v), and reuse t(v,V(v)) for the extra copies needed only to meet the QFBAPA cardinality constraints, relying on the feature-value copying described in the definition of f^I. With that correction, Lemma 6 and the feature-value argument in Lemma 7 appear to go through; without it, the soundness direction of Theorem 2 is incomplete.
minor comments (3)
  1. [Lemma 4 proof, Appendix B] The sentence about 'unconnected elements from Δ_{I''} \ Δ_{I'}' should refer to Δ_{I'} \ Δ_{I''}, since Δ_{I''} is the reachable subdomain and the omitted elements are those outside it.
  2. [Lemma 4 proof, Appendix B] The notation 'NR(O)' is not defined; it should be either the set of role names of the ontology or an explicit subset of NR.
  3. [Lemma 2, §4] The proof would be easier to follow if the loop variable j (the index of the successor copy) and the patch index i were not made to coincide indirectly; after switching to i = min(j,V(v)), the two indices should be named consistently throughout Lemma 2 and Lemma 6.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the ExpTime upper bound is a genuine construction, not an unpacking of the assumptions.

full rationale

The central claim, Theorem 2, is conditional on D being ExpTime-omega-admissible, i.e., on CSP(D) being in ExpTime; it then proves by a type-elimination algorithm that consistency in ALCOSCC(D) is in ExpTime. The DL consistency problem is not defined as the output of that algorithm: consistency has an independent model-theoretic semantics, and Lemmas 2 and 3 establish soundness and completeness of Algorithm 1. The construction genuinely builds a model from surviving augmented types and uses homomorphism omega-compactness for the concrete domain, so the upper bound is not the input assumption restated. Self-citations are present — Lemma 1 cites [3] for the strengthened QFBAPA Venn-region bound, and the concrete-domain framework cites [26,10,12] — but those are published theorems with independent proofs and are used as lemmas, not as the sole justification of the main result; no uniqueness claim is imported to force the choice. Definition 1 is a deliberate strengthening (the paper says it 'differ[s] from omega-admissible ones ... by a stronger requirement'), not an ansatz smuggled by citation. The skeptical concern about Lemma 2 (using i = max(j,V(v)) rather than a patch at every required (v,j)) is a potential soundness gap in the model construction, but it is not a circular reduction: it does not identify any predicted quantity with a fitted input or define the target in terms of the proof. Accordingly, no circular step is exhibited.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The paper introduces new syntax (feature pointers, feature roles, succ-restrictions over feature roles) but no new domain entities, no new physical constants, and no fitted parameters. The introduced formalism is defined within the paper, so it is not an unsupported entity.

assumptions (6)
  • standard math QFBAPA satisfiability is NP-complete and Lemma 1's polynomial bound N_phi holds.
    Used throughout Section 4 and Algorithm 1 to bound Venn bags and check satisfiability of phi_t,V; result from Kuncak-Rinard [21] and strengthened in Baader [3].
  • standard math ALC consistency is ExpTime-hard.
    Used for the lower bound in Theorem 2; attributed to Schild [29].
  • domain assumption There exist concrete domains D satisfying Definition 1, such as Q, Allen's interval algebra, and RCC8.
    The main theorem is conditional on D being ExpTime-omega-admissible; these conditions (finite signature, patchwork, homomorphism omega-compactness, CSP in ExpTime) are strong and not satisfied by all concrete domains.
  • domain assumption Known omega-admissible concrete domains are homogeneous.
    Used in Lemma 5 and Theorem 3 to reduce feature assertions with constants to predicate assertions.
  • standard math Undecidability of ALC(D) with the concrete domain (N,+1) and undecidability of tiling problems.
    Used for the undecidability reductions in Section 6, Theorems 4 and 6.
  • domain assumption The domain set of D is infinite and D is JD for the undecidable extensions.
    Section 6 states 'we assume that the domain set of D is infinite and that D is JD' for the undecidability results.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)." pith.science (2026). https://pith.science/paper/PSEXSHQ6

@misc{pith2026250521103,
  author       = {Pith},
  title        = {Pith review of: Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PSEXSHQ6}},
  note         = {Machine review of arXiv:2505.21103}
}
abstract

Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete domains, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in $\mathcal{ALCSCC}$, while the comparison of feature values of different individuals in $\mathcal{ALC}(\mathfrak{D})$ has been studied in the context of $\omega$-admissible concrete domains $\mathfrak{D}$. In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL $\mathcal{ALCOSCC}(\mathfrak{D})$, which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of $\mathfrak{D}$ is also decidable in exponential time. It is thus not higher than the complexity of the basic DL $\mathcal{ALC}$. At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.

Figures

Figures reproduced from arXiv: 2505.21103 by the authors.

Figure 1
Figure 1. A representation of the structure enforced using transitive roles. For every model I of TP we want to ensure that every v-successor of a h-successor of d ∈ ∆I is also a role successor of d, and similarly for every h-successor of a v-successor. As I must be finitely branching, though, it is not possible to simply use one transitive role r that includes both h and v, as this would imply that d has infinitely many succ… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

33 extracted references · 28 canonical work pages

  1. [3]

    In: Dixon, C., Finger, M

    Baader, F.: A new description logic with set constraints and cardinality con- straints on role successors. In: Dixon, C., Finger, M. (eds.) Proc. of the 11th Int. Symposium on Frontiers of Combining Systems (FroCoS’17). Lecture Notes in Computer Science, vol. 10483, pp. 43–59. Springer-Verlag, Brasília, Brazil (2017). https://doi.org/10.1007/978-3-319-66167-4_3

    work page doi:10.1007/978-3-319-66167-4_3 2017

  2. [12]

    In: Giordano, L., Jung, J.C., Ozaki, A

    Borgwardt, S., De Bortoli, F., Koopmann, P.: The precise complexity of reasoning in ALC with ω-admissible concrete domains. In: Giordano, L., Jung, J.C., Ozaki, A. (eds.) Proceedings of the 37th International Workshop on Description Logics (DL 2024). CEUR Workshop Proceedings, vol. 3739. CEUR-WS.org (2024), https: //ceur-ws.org/Vol-3739/paper-1.pdf

    work page 2024

  3. [1]

    Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983). https://doi.org/10.1145/182.358434

    doi:10.1145/182.358434 1983

  4. [2]

    In: Fensel, A., Ozaki, A., Roman, D., Soylu, A

    Alrabbaa,C.,Baader,F.,Borgwardt,S.,Koopmann,P.,Kovtunova,A.:Combining proofs for description logic and concrete domain reasoning. In: Fensel, A., Ozaki, A., Roman, D., Soylu, A. (eds.) Rules and Reasoning - 7th International Joint Con- ference, RuleML+RR 2023, Proceedings. Lecture Notes in Computer Science, vol. 14244, pp. 54–69. Springer (2023). https://...

    work page doi:10.1007/978-3-031-45072-3_4 2023

  5. [4]

    In: ECAI 2020

    Baader, F., Bednarczyk, B., Rudolph, S.: Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints. In: ECAI 2020. pp. 616–623. IOS Press (2020). https://doi.org/10.3233/FAIA200146

    work page doi:10.3233/faia200146 2020

  6. [5]

    (eds.): The Description Logic Handbook: Theory, Implementation, and Applications

    Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003). https://doi.org/10.1017/ CBO9780511711787

    work page 2003

  7. [6]

    In: Herzig, A., Popescu, A

    Baader, F., De Bortoli, F.: On the expressive power of description logics with cardinality constraints on finite and infinite sets. In: Herzig, A., Popescu, A. (eds.) Frontiers of Combining Systems – 12th International Symposium, FroCoS 2019, Proceedings. Lecture Notes in Computer Science, vol. 11715, pp. 203–219. Springer (2019). https://doi.org/10.1007/...

    work page doi:10.1007/978-3-030-29007-8_12 2019

  8. [7]

    In: Mylopoulos, J., Reiter, R

    Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th Interna- tional Joint Conference on Artificial Intelligence, IJCAI 1991. pp. 452–457. Morgan Kaufmann (1991), http://ijcai.org/Proceedings/91-1/Papers/070.pdf

    work page 1991

Show all 33 references
  1. [8]

    Cambridge UniversityPress (2017).https://doi.org/10.1017/9781139025355

    Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge UniversityPress (2017).https://doi.org/10.1017/9781139025355

    2017 doi

  2. [9]

    In: Peltier, N., Sofronie-Stokkermans, V

    Baader, F., Rydval, J.: Description logics with concrete domains and general con- cept inclusions revisited. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Auto- mated Reasoning – 10th International Joint Conference, IJCAR 2020, Proceed- ings, Part I. Lecture Notes in Comput...

    2020 doi

  3. [10]

    Journal of Automated Reasoning66(3), 357–407 (Aug 2022)

    Baader, F., Rydval, J.: Using Model Theory to Find Decidable and Tractable De- scription Logics with Concrete Domains. Journal of Automated Reasoning66(3), 357–407 (Aug 2022). https://doi.org/10.1007/s10817-022-09626-2

    2022 doi

  4. [11]

    Memoirs of the American Mathematical Society 66, 72 (1966), https://mathscinet.ams.org/ mathscinet-getitem?mr=216954

    Berger, R.: The undecidability of the domino problem. Memoirs of the American Mathematical Society 66, 72 (1966), https://mathscinet.ams.org/ mathscinet-getitem?mr=216954

    1966

  5. [13]

    general tboxes is decidable for concrete domains with the ehd-property

    Carapelle, C., Turhan, A.: Description logics reasoning w.r.t. general tboxes is decidable for concrete domains with the ehd-property. In: Kaminka, G.A., Fox, M., Bouquet, P., Hüllermeier, E., Dignum, V., Dignum, F., van Harmelen, F. (eds.) ECAI 2016 – 22nd European Conference...

    2016 doi

  6. [14]

    In: Gaggl, S.A., Martinez, M.V., Ortiz, M

    Demri, S., Quaas, K.: First steps towards taming description logics with strings. In: Gaggl, S.A., Martinez, M.V., Ortiz, M. (eds.) Logics in Artificial Intelligence – 18th European Conference, JELIA 2023, Proceedings. Lecture Notes in Com- puter Science, vol. 14281, pp. 322–3...

    2023

  7. [15]

    In: Singh, S., Markovitch, S

    Gutiérrez-Basulto, V., Ibáñez-García, Y.A., Jung, J.C.: Number restrictions on transitive roles in description logics with nominals. In: Singh, S., Markovitch, S. (eds.) Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence. pp. 1121–1127. AAAI Press (2017...

    2017 doi

  8. [16]

    In: Allen, J.F., Fikes, R., Sandewall, E

    Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Allen, J.F., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR’91). pp. 335–346. Morgan Kaufmann (1991)

    1991

  9. [17]

    Hollunder, B., Nutt, W., Schmidt-Schauß, M.: Subsumption algorithms for concept descriptionlanguages.In:9thEuropeanConferenceonArtificialIntelligence,ECAI

  10. [18]

    In: Nebel, B

    Horrocks, I., Sattler, U.: Ontology reasoning in theSHOQ (D) description logic. In: Nebel, B. (ed.) Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001. pp. 199–204. Morgan Kaufmann (2001)

    2001

  11. [19]

    Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive descrip- tion logics. Log. J. IGPL8(3), 239–263 (2000). https://doi.org/10.1093/JIGPAL/ 8.3.239

    2000 doi

  12. [20]

    Artificial Intelligence257, 1–23 (Apr 2018)

    Jonsson, P.: Constants and finite unary relations in qualitative constraint reason- ing. Artificial Intelligence257, 1–23 (Apr 2018). https://doi.org/10.1016/j.artint. 2017.12.003

    2018 doi

  13. [21]

    In: Pfenning, F

    Kuncak, V., Rinard, M.: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. In: Pfenning, F. (ed.) Automated Deduc- tion – CADE-21. Lecture Notes in Computer Science, vol. 4603, pp. 215–230. Springer Berlin Heidelberg, Berlin, Heidelberg (...

    2007

  14. [22]

    In: Calvanese, D., Erdem, E., Thielscher, M

    Labai, N., Ortiz, M., Simkus, M.: An ExpTime upper bound forALC with integers. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th Inter- national Conference on Principles of Knowledge Representation and Reasoning, KR 2020. pp. 614–623 (2020). https://d...

    2020 doi

  15. [23]

    Artificial Intelligence201, 32–58 (Aug 2013)

    Li,S.,Liu,W.,Wang,S.:Qualitativeconstraintsatisfactionproblems:Anextended framework with landmarks. Artificial Intelligence201, 32–58 (Aug 2013). https: //doi.org/10.1016/j.artint.2013.05.006

    2013 doi

  16. [24]

    Lutz, C.: The complexity of description logics with concrete domains. Ph.D. thesis, RWTH Aachen University, Germany (2002), http://sylvester.bth.rwth-aachen.de/ dissertationen/2002/042/index.htm

    2002

  17. [25]

    ACM Transactions on Computational Logic (TOCL)5(4), 669–705 (2004)

    Lutz, C.: NExpTime-complete description logics with concrete domains. ACM Transactions on Computational Logic (TOCL)5(4), 669–705 (2004). https://doi. org/10.1145/1024922.1024925

    2004

  18. [26]

    Journal of Automated Reasoning38(1), 227–259 (Apr 2007)

    Lutz, C., Miličić, M.: A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes. Journal of Automated Reasoning38(1), 227–259 (Apr 2007). https://doi.org/10.1007/s10817-006-9049-7

    2007 doi

  19. [27]

    With a foreword by Martin Davis

    Matiyasevich, Y.V.: Hilbert’s tenth problem. With a foreword by Martin Davis. Cambridge, MA: MIT Press (1993)

    1993

  20. [28]

    In: Nebel, B., Rich, C., Swartout, W.R

    Randell,D.A.,Cui,Z.,Cohn,A.G.:Aspatiallogicbasedonregionsandconnection. In: Nebel, B., Rich, C., Swartout, W.R. (eds.) Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR’92). pp. 165–176. Morgan Kaufmann (1992)

    1992

  21. [29]

    In: Mylopoulos, J., Reiter, R

    Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI’91). pp. 466–471. Morgan Kaufmann (1991), http://ijcai.org/Proceedi...

    1991

  22. [30]

    Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artif. Intell. Res.12, 199–217 (2000). https: //doi.org/10.1613/JAIR.705

    2000 doi

  23. [31]

    Tobies, S.: PSPACE reasoning for graded modal logics. J. Log. Comput.11(1), 85–106 (2001). https://doi.org/10.1093/LOGCOM/11.1.85 A Deciding Consistency — Auxiliary Results The proofs of Lemma 2 and Lemma 3 depend on a series of lemmas that we provide in this section. A.1 Soun...

    2001 doi

  24. [32]

    , pk.P ∈ tI(d) iff (c1,

    We have ∃p1, . . . , pk.P ∈ tI(d) iff (c1, . . . , ck) ∈ P D for some values ci ∈ pI i (d)with i = 1, . . . , k; by construction ofVd, ifpi = rifi we can findei ∈ Scd such that (d, ei) ∈ rI i and f I i (ei) =ci, and setxi := λ−1 d (ei); if pi = fi (and f I i (d) = ci), we set ...

  25. [33]

    We know thatv = ve for some individuale = λd(x) with x ∈ Xd, and thus XP (α1,...,αk) ∈ v = ve iff αI 1 (d, e),

    Consider any variable of the formXP (α1,...,αk), a Venn regionv ∈ supp(Vd) and 1 ≤ j ≤ Vd(v). We know thatv = ve for some individuale = λd(x) with x ∈ Xd, and thus XP (α1,...,αk) ∈ v = ve iff αI 1 (d, e), . . . , αI k (d, e) ∈ P D. Setting xi := ι(tI(d)) if αi = fi and xi := x...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.