Fuzzy Lattice-based Description Logic

Krishna Manoorkar; Yiwen Ding

REVIEW 2 major objections 6 minor 25 references

Fuzzy Lattice-based Description Logic

T0 review · 2 major / 6 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 This paper introduces LE-FALC, a fuzzy generalization of the non-distributive description logic LE-ALC, and proves that a non-branching tableaux algorithm decides ABox consistency in polynomial time.

desk verdict LE-FALC is a natural fuzzy extension of LE-ALC, but the polynomial-time and completeness claims both rest on gaps that need fixing. read the letter →

arxiv 2506.05833 v1 pith:6B77JX6N submitted 2025-06-06 cs.LO cs.AI

Yiwen Ding , Krishna Manoorkar This is my paper

classification cs.LOcs.AI MSC 03B5003B4503G1068T27

keywords fuzzydescriptionlogicnon-distributiveformalconceptanalysistableauxalgorithmmany-valuedHeytingalgebraconsistencydecisionprocedurelattice-based

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

The paper introduces LE-FALC, a description logic for reasoning about fuzzy formal concepts—categories of objects and features with graded membership—in the setting of many-valued enriched formal contexts. It claims that checking consistency of LE-FALC ABoxes can be decided by a sound and complete tableaux algorithm in polynomial time, and that an exponential-time procedure for acyclic TBoxes follows by unraveling. The interest is that this extends automated reasoning for description logics to a genuinely fuzzy, non-distributive lattice-based setting, where concepts are pairs of fuzzy sets of objects and features rather than sets. If correct, the algorithm provides an efficient route to standard reasoning tasks such as instance checking and subsumption for knowledge bases describing vague categories.

What carries the argument

The central machinery is Algorithm 2, a non-branching tableaux whose assertions are graded inequalities over a complete Heyting algebra $H$. For each concept $C$ occurring in the ABox, the creation rule introduces a classifying object $a_C$ and a classifying feature $x_C$; the I-compatibility rules add adjoint witnesses $\blacklozenge b$, $\Diamond b$, $\square y$, $\blacksquare y$ so that the modal relations are compatible with the incidence relation, making the constructed structure an $H$-valued enriched formal context. The rule MV∨, which derives $\alpha_1 \vee \alpha_2 \leq t$ from $\alpha_1 \leq t$ and $\alpha_2 \leq t$, is the only graded addition to the crisp algorithm and keeps the tableau growth linear. Lemma 3 shows that the interpretation of every concept is pinned down by the inequalities involving its classifying object and feature, and Lemma 4—the proof of which is omitted—asserts that any model can be extended to one with such classifiers and adjoint witnesses.

What would settle it

Exhibit a finite complete Heyting algebra $H$ and an LE-FALC ABox with a model for which no extension to fresh constants $a_C$, $x_C$, $\blacklozenge b$, $\Diamond b$, $\square y$, $\blacksquare y$ satisfies equations (6) and (7). Concretely, one could compute the required adjoint witnesses for the three-valued example in the paper and check the equalities defining the adjoints; a failure of these equalities would refute Lemma 4 and break the completeness argument for Algorithm 2.

Watch

Extended reading notes

Core claim

LE-FALC is interpreted on $H$-valued enriched formal contexts, where $H$ is a complete and completely distributive Heyting algebra, and every concept $C$ receives an extension (a fuzzy set of objects) and an intension (a fuzzy set of features). The paper's central claim is that the crisp LE-ALC tableaux rules lift to this graded setting by reading assertions as inequalities $\alpha \leq t$ and $\alpha \not\leq t$, adding a many-valued join rule MV∨ that merges lower bounds, and supplying fresh classifying objects $a_C$ and features $x_C$ together with adjoint witnesses $\blacklozenge b$, $\Diamond b$, $\square y$, $\blacksquare y$ to enforce Galois stability. The resulting non-branching tableaux terminates in polynomial time and is sound (Theorem 3) and complete (Theorem 4) for ABox consistency. The paper also states, without proof, that unraveling acyclic TBoxes yields an exponential-time decision procedure.

Load-bearing premise

The completeness proof depends on Lemma 4, which asserts that every model of an ABox can be extended with classifying objects, classifying features, and adjoint witnesses to satisfy the adjunction properties; the paper states only 'It is straightforward to check' and provides no proof.

Editorial extensions

If this is right

Algorithm 2 decides consistency of LE-FALC ABoxes in polynomial time.
Every consistent LE-FALC ABox has a model of polynomial size (finite model property).
Acyclic TBoxes can be handled in exponential time by unraveling, extending the ABox decision procedure to knowledge bases.
Because standard description-logic reasoning tasks reduce to consistency, the tableaux gives an efficient route to instance checking and subsumption for LE-FALC.
The tableaux is non-branching, so the consistency test avoids exponential branching from disjunction and diamond operators.

Reading between the lines

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

A natural testable extension is to run the same graded tableaux over other complete residuated lattices, since the soundness proof uses only completeness and distributivity of $H$; the paper notes such generality is possible but does not work it out.
The explicit admissibility of the MV∨ rule suggests the polynomial bound can be made concrete with a low-degree exponent, though the paper does not compute one.
If Lemma 4 were to fail for some residuated lattice, only the completeness half of the algorithm would be affected; soundness and termination would still hold.
The graded framework could support "to what degree" entailment queries by tracking maximal thresholds in a completed tableau, a capability the paper does not discuss.

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.

Desk Editor's Note

read the letter

First reaction: this is a sensible fuzzy generalization of LE-ALC, and the basic semantic setup is coherent. The language, the two-sorted ABox, and the tableaux rules all carry over cleanly from the crisp case, and the examples in Section 4 do show how the logic handles non-distributive reasoning about fuzzy concepts. The soundness proof in Section 6 looks plausible, and Lemma 3, which links ABox assertions to the constructed model, is actually worked out in the appendix. If the gaps below are patched, this would be a solid contribution to lattice-based and fuzzy description logics.

The soft spots are real. First, the termination argument for Algorithm 2 is wrong as written. The paper claims the MV∨ rule can only increase the tableau linearly, but the rule from α1≤t and α2≤t to α1∨α2≤t forces saturation under binary joins. With n incomparable values e1,...,en in the Heyting algebra and assertions ei≤I(a,x), every completion must contain (∨_{i∈S} ei)≤I(a,x) for each nonempty S, which is 2^n−1 terms for a single relational term. That is exponential, not linear, so Theorem 2 is unsupported. A repair—merging premises into their join and deleting them—might restore a polynomial bound, but it is not stated or proved. Second, Lemma 4, the model-extension lemma on which completeness depends, is dismissed with "It is straightforward to check." That is not adequate for a construction that must add classifying objects, adjoint witnesses, and verify I-compatibility plus all semantic clauses. Third, the acyclic TBox extension is only a remark, so the exponential-time claim for TBoxes is also unproven.

None of this makes the approach look fundamentally broken. The definitions are reasonable and the proof strategy is a natural continuation of the authors' earlier work. But as it stands, the two headline theorems are not backed by valid arguments. I'd send this to peer review, but with the expectation of serious revision: the termination proof needs to be redone, and Lemma 4 needs a full proof. Researchers in non-distributive and fuzzy DLs will want the corrected version.

Referee Report

2 major / 6 minor

Summary. The paper introduces LE-FALC, a fuzzy (many-valued) generalization of the non-distributive description logic LE-ALC, with semantics based on H-valued enriched formal contexts. It defines a tableaux algorithm (Algorithm 2) for checking consistency of LE-FALC ABoxes and claims that the algorithm is sound, complete, and runs in polynomial time (Theorems 2, 3, and 4). It further claims an exponential-time decision procedure for knowledge bases with acyclic TBoxes via unraveling. The paper includes two examples demonstrating the algorithm and appendix proofs of the soundness lemma (Lemma 3).

Significance. If the technical gaps are repaired, this is a useful contribution: it connects fuzzy formal concept analysis with description logics and extends the authors' earlier LE-ALC framework to many-valued semantics. The tableaux design is non-branching, the model construction in the soundness proof is concrete, and the worked examples illustrate the formalism. However, the two main technical pillars—the polynomial-time bound and the completeness lemma—are not currently established rigorously, so the significance is conditional on a successful revision.

major comments (2)

[Section 7, Lemma 4] Lemma 4 underpins Theorem 4 (Completeness), yet its proof consists only of the sentence 'It is straightforward to check that M′ is a model for A and satisfies all the properties required in Lemma 4.' To be complete, the proof must verify (i) that the relations R′✷ and R′✸ defined in the four cases are I′-compatible in the sense of Definition 2; (ii) that equations (6) and (7) hold with the chosen definitions of ◆b, ✸b, ✷y, ■y; and (iii) that the truth of all ABox assertions is preserved under the extension. None of these checks is carried out, so the completeness theorem is not established by the text.
[Section 5, Theorem 2 / MV∨ rule] The termination proof of Theorem 2 relies on the assertion in Section 5 that the rule MV∨ 'can only increase the size of tableau linearly.' This is false: closure under binary joins is forced by saturation. For instance, let H be the Boolean algebra with n atoms e_1,...,e_n and let the input ABox contain the assertions e_i ≤ I(a,x) for i=1,...,n. Any saturated completion must contain (⋁_{i∈S} e_i) ≤ I(a,x) for every nonempty S ⊆ {1,...,n}, i.e., 2^n−1 distinct terms for a single relational term, contradicting the claimed linear bound and invalidating the polynomial-time statement of Theorem 2 as written. A modification of the rule (e.g., merging α1≤t and α2≤t into α1∨α2≤t and deleting the premises) might repair the polynomial bound, but the algorithm and proof as stated do not include such a strategy.

minor comments (6)

[Section 3] In the sentence 'A knowledge base in LE-FALC is a tuple (A,T), where A is an LE-ALC ABox, and T is an LE-ALC TBox,' the two occurrences of 'LE-ALC' should read 'LE-FALC.'
[Section 6] In step 2 of the model construction, the value of I(a,x) is defined as the maximum of the α_i for which α_i ≤ I(a,x) occurs in the completion, but the case where no such assertion exists is not handled; the default value should be stated explicitly (e.g., 0).
[Abstract and Section 5] The exponential-time decision procedure for acyclic TBoxes by unraveling is claimed in the abstract but only stated as an unproved remark in Section 5; either provide a proof or label it as a conjecture or future work.
[Appendix A.1] The proof of Lemma 3 uses the phrase 'by completeness of H' in several places; the intended justification is unclear and should be replaced with a precise reference to a lattice-theoretic property (e.g., the finite join-closure of the sets of degrees ensured by MV∨).
[Section 7, Lemma 4] In the definition of R′✸, the argument order is R′✸(x,a) but the text sometimes refers to R′✸(a,x); the notation should be made consistent throughout.
[Throughout] There are several typos, e.g., 'It sucffices' in Lemma 1 and 'for for any' in Appendix A.1; the manuscript would benefit from a careful proofreading.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the fuzzy tableaux derivation is self-contained; the unproved Lemma 4 and the MV∨ termination argument are proof gaps, not circular reasoning.

full rationale

The paper's central claim, that Algorithm 2 is a sound and complete polynomial-time decision procedure for LE-FALC ABox consistency, is not obtained by assuming the conclusion. The tableaux rules, the model construction in Section 6, and the completeness argument in Section 7 are developed from the semantics of many-valued LE-logic and from the crisp LE-ALC framework, not from the fuzzy theorem being proved. The termination proof does rely on a citation to the authors' prior work [8] — 'the polynomial time termination result for LE-FALC tableaux algorithm follows from the termination result for LE-ALC tableaux algorithm (See [8, Section 4.1], for more details)' — but [8] is a separately published, previously established result for the crisp logic LE-ALC, so invoking it is legitimate evidence rather than a circular reduction of the fuzzy claim to itself. The proof of Lemma 4 is omitted ('It is straightforward to check'), and the MV∨ termination argument ('this rule can only increase the size of tableau linearly') is questionable because closure under binary joins can generate exponentially many terms; however, these are correctness and soundness gaps, not instances of a result being defined or fitted into existence. I find no step where an equation, parameter, or model is constructed so that the claimed theorem holds by definition, and no renamed empirical pattern is presented as a derivation.

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

The paper introduces no fitted parameters. The semantic framework assumes a complete completely distributive Heyting algebra H and I-compatible fuzzy relations. The completeness proof relies on an unproved model-extension lemma (Lemma 4) that postulates classifying objects/features and adjoint witnesses. The new constants ◆b, ✸b, ✷y, ■y are syntactic proof artifacts and are not postulated semantic entities. The paper's central decidability results hold only for the restricted concept language without ⊤ and ⊥.

assumptions (4)

domain assumption H is a complete and completely distributive Heyting algebra with residual implication.
The entire semantics is built over such H; the paper notes in footnote 2 that results generalize to complete frame-distributive and dually frame-distributive commutative associative residuated lattices, but the proofs are only given for Heyting algebras.
domain assumption The relations R✷ and R✸ in H-valued enriched formal contexts are I-compatible.
Definition 2 requires I-compatibility to ensure modal operators are well-defined on the concept lattice; the tableaux rules and model construction rely on this.
ad hoc to paper Lemma 4: every model of an ABox can be extended with classifying objects/features and adjoint witnesses satisfying properties (5)-(7).
This model-extension lemma is essential for completeness but is stated without proof. It postulates the existence of new elements with specific properties, and the paper does not provide the detailed verification.
domain assumption The restricted language without ⊤ and ⊥ is sufficient; adding them can cause non-termination.
The paper excludes ⊤ and ⊥ from the concept language because tableaux rules for them lead to non-termination, as noted in the introduction and Section 2.3. The central result is only for this restricted language.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Fuzzy Lattice-based Description Logic." pith.science (2026). https://pith.science/paper/6B77JX6N

@misc{pith2026250605833,
  author       = {Pith},
  title        = {Pith review of: Fuzzy Lattice-based Description Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6B77JX6N}},
  note         = {Machine review of arXiv:2506.05833}
}

read the original abstract

Recently, description logic LE-ALC was introduced for reasoning in the semantic environment of enriched formal contexts, and a polynomial-time tableaux algorithm was developed to check the consistency of knowledge bases with acyclic TBoxes. In this work, we introduce a fuzzy generalization of LE-ALC called LE-FALC which provides a description logic counterpart of many-valued normal non-distributive logic a.k.a. many-valued LE-logic. This description logic can be used to represent and reason about knowledge in the formal framework of fuzzy formal contexts and fuzzy formal concepts. We provide a tableaux algorithm that provides a complete and sound polynomial-time decision procedure to check the consistency of LE-FALC ABoxes. As a result, we also obtain an exponential-time decision procedure for checking the consistency of LE-FALC with acyclic TBoxes by unraveling.

Figures

Figures reproduced from arXiv: 2506.05833 by the authors.

**Figure 1.** The concept lattice of (A,X,I) M,a α p iff α ≤ [[p]](a); M,a α ⊤ iff α ≤ (1 HA )(a) i.e. always; M,a α ⊥ iff α ≤ (1 HX ) ↓ (a) = V x∈X (1 HX (x) → I(a,x)) = V x∈X I(a,x); M,a α ϕ ∧ψ iff M,a α ϕ and M,a α ψ; M,a α ϕ ∨ψ iff α ≤ (([ϕ])∧([ψ]))↓ (a) = V x∈X (([ϕ])(x)∧([ψ])(x) → I(a,x)); M,a α ✷ϕ iff α ≤ (R (0) ✷ [([ϕ])])(a) = V x∈X (([ϕ])(x) → R✷(a,x)); M,a α ✸ϕ iff α ≤ ((R (0) ✸ [[[ϕ]]])↓ )(a) = V x∈X ((R (0) ✸ [[[ϕ]]])… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

25 extracted references · 21 canonical work pages

[1]

IEEE Transactions on Systems, Man, and Cybernetics: Systems 44(5), pp

Jamal Atif, Celine Hudelot & Isabelle Bloch (2014): Explanatory Reasoning for Image Understanding Using F ormal Concept Analysis and Description Logics . IEEE Transactions on Systems, Man, and Cybernetics: Systems 44(5), pp. 552–570, doi: 10.1109/TSMC.2013.2280440

work page arXiv 2014
[2]

Cambridge university press

Franz Baader (2003): The description logic handbook: Theory, implementation an d applications. Cambridge university press

work page 2003
[3]

Cambridge University Press, doi:10.1017/9781139025355

Franz Baader, Ian Horrocks, Carsten Lutz & Uli Sattler (2 017): Introduction to description logic. Cambridge University Press, doi:10.1017/9781139025355

doi:10.1017/9781139025355
[4]

Concept Lattices, pp

Franz Baader & Baris Sertkaya (2004): Applying F ormal Concept Analysis to Description Logics . Concept Lattices, pp. 261–286, doi: 10.1007/978-3-540-24651-0_24

work page doi:10.1007/978-3-540-24651-0_24 2004
[5]

Mathematical Logic Quarterly 45(4), pp

Radim Bˆ elohl´ avek (1999):Fuzzy Galois Connections . Mathematical Logic Quarterly 45(4), pp. 497–504, doi:10.1002/malq.19990450408

work page doi:10.1002/malq.19990450408 1999
[6]

Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2023): Labelled Calculi for the Logics of Rough Concepts

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, K rishna B. Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2023): Labelled Calculi for the Logics of Rough Concepts . Logic and Its Applications , pp. 172–188, doi: 10.1007/978-3-031-26689-8_13

work page doi:10.1007/978-3-031-26689-8_13 2023
[7]

In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer Nature Switzerland Cham, pp

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, K rishna B Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2023): Non-distributive description logic . In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer Nature Switzerland Cham, pp. 49–69, doi:10.1007/978-3-031-43513-3_4

work page doi:10.1007/978-3-031-43513-3_4 2023
[8]

Non-distributive description logic

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, K rishna B. Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2024): Non-distributive description logic. arXiv: 2307.09561. Y . Ding, K. Manoorkar 59

work page Pith review arXiv 2024

Show all 25 references

[9]

Information Sciences 561, pp

Willem Conradie, Sabine Frittella, Krishna Manoorkar, Sajad Nazari, Alessandra Palmigiano, Apostolos Tz- imoulis & Nachoem M Wijnberg (2021): Rough concepts. Information Sciences 561, pp. 371–413, doi: 10. 1016/j.ins.2020.05.074

2021
[10]

In: Logic, Language, Information, and Computation: 23rd Internation al Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016

Willem Conradie, Sabine Frittella, Alessandra Palmig iano, Michele Piazzai, Apostolos Tzimoulis & Na- choem M Wijnberg (2016): Categories: how I learned to stop worrying and love two sorts . In: Logic, Language, Information, and Computation: 23rd Internation al Workshop, WoLLI...

2016 doi
[11]

arXiv preprint arXiv:1707.08743

Willem Conradie, Sabine Frittella, Alessandra Palmig iano, Michele Piazzai, Apostolos Tzimoulis & Nachoem M Wijnberg (2017): T oward an epistemic-logical theory of categorization . arXiv preprint arXiv:1707.08743

2017 arXiv
[12]

arXiv preprint arXiv:1908.04816

Willem Conradie, Alessandra Palmigiano, Claudette Ro binson, Apostolos Tzimoulis & Nachoem M Wijn- berg (2019): The logic of vague categories . arXiv preprint arXiv:1908.04816

2019 arXiv
[13]

arXiv preprint arXiv:2002.04257

Willem Conradie, Alessandra Palmigiano, Claudette Ro binson & Nachoem Wijnberg (2020): Non- distributive logics: from semantics to meaning . arXiv preprint arXiv:2002.04257

2020 arXiv
[14]

In: In General Lattice Theory, G

Bernhard Ganter & Rudolf Wille (1997): Applied lattice theory: F ormal concept analysis . In: In General Lattice Theory, G. Gr¨ atzer editor, Birkh¨ auser, Citeseer

1997
[15]

Springer Science & Business Media

Bernhard Ganter & Rudolf Wille (2012): F ormal concept analysis: mathematical foundations . Springer Science & Business Media

2012
[16]

Journal of Logic and Computation 28(7), p

Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Ap ostolos Tzimoulis & Zhiguang Zhao (2016): Uni- ﬁed correspondence as a proof-theoretic tool . Journal of Logic and Computation 28(7), p. 1367–1442

2016
[17]

Kluwer Academic Publishers, Dordrecht, Boston and London, doi:10.1007/978-94-011-5300-3

Petr H´ ajek (1998): Metamathematics of Fuzzy Logic . Kluwer Academic Publishers, Dordrecht, Boston and London, doi:10.1007/978-94-011-5300-3

1998 doi
[18]

Knowledge-Based Systems 186, doi:10.1016/j.knosys.2019.104967

Y uncheng Jiang (2019): Semantifying formal concept analysis using description lo gics. Knowledge-Based Systems 186, doi:10.1016/j.knosys.2019.104967

2019
[19]

Kuznetsov Jonas Poelmans, Dmitry I

Sergei O. Kuznetsov Jonas Poelmans, Dmitry I. Ignatov & Guido Dedene (2014): Fuzzy and rough formal concept analysis: a survey . International Journal of General Systems 43(2), pp. 105–134, doi: 10.1080/ 03081079.2013.862377

2014
[20]

Expert systems with applications 40(16), pp

Jonas Poelmans, Sergei O Kuznetsov, Dmitry I Ignatov & G uido Dedene (2013): F ormal concept analysis in knowledge processing: A survey on models and techniques . Expert systems with applications 40(16), pp. 6601–6623, doi: 10.1016/j.eswa.2013.05.007. A Proofs In this appendix...

2013 doi
[21]

Suppose C = C1 ∧C2. 1.1. For the ﬁrst claim, it is required to prove that max{ α | α ≤ I(b,xC1∧C2) ∈ A } = [ [C1 ∧C2] ](b). 60 Fuzzy Lattice-based Description Logic For direction (≤), suppose α 0 ≤ bIxC1∧C2 ∈ A for some α 0. Then by using appending and ∧A rules, we have α 0 ≤ ...
[22]

The proof for C = C1 ∨C2 is similar to the previous one
[23]

Suppose C = [R✷]C1. 3.1. For the ﬁrst claim, it is required to prove that [ [[R✷]C1] ](b) = max{β | β ≤ I(b,x✷C1) ∈ A }. For direction (≤), notice that [ [[R✷]C1] ](b) = ⋀ y∈X (( [C1] )(y) → R✷(b,y)). By induction and con- struction of the model, this is equivalent to [ [[R✷]C...
[24]

This concludes the proof

The proof for C = ⟨R✸⟩C1 is similar to the previous one. This concludes the proof. B Model for the ﬁrst example knowledge base In this section, we describe model for the ﬁrst knowledge bas e deﬁned in Section 4 obtained using unraveling and Tableaux Algorithm 2. Let K = (A ,T ...
[25]

By substituting these deﬁnitions in ABox and running Algori thm 2, we get a model for K using con- struction described in Section 6

C6 ≡ (C1 ∧ ((C1 ∨C3) ∧C7)) ∨ (((C1 ∨C3) ∧C7) ∧C3) ≡ (C1 ∧C7) ∨ (C7 ∧C3). By substituting these deﬁnitions in ABox and running Algori thm 2, we get a model for K using con- struction described in Section 6. Table 1 lists symbols we us e for different constants of the form aC or...

Pith tools

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

[1] [1]

IEEE Transactions on Systems, Man, and Cybernetics: Systems 44(5), pp

Jamal Atif, Celine Hudelot & Isabelle Bloch (2014): Explanatory Reasoning for Image Understanding Using F ormal Concept Analysis and Description Logics . IEEE Transactions on Systems, Man, and Cybernetics: Systems 44(5), pp. 552–570, doi: 10.1109/TSMC.2013.2280440

work page arXiv 2014

[2] [2]

Cambridge university press

Franz Baader (2003): The description logic handbook: Theory, implementation an d applications. Cambridge university press

work page 2003

[3] [3]

Cambridge University Press, doi:10.1017/9781139025355

Franz Baader, Ian Horrocks, Carsten Lutz & Uli Sattler (2 017): Introduction to description logic. Cambridge University Press, doi:10.1017/9781139025355

doi:10.1017/9781139025355

[4] [4]

Concept Lattices, pp

Franz Baader & Baris Sertkaya (2004): Applying F ormal Concept Analysis to Description Logics . Concept Lattices, pp. 261–286, doi: 10.1007/978-3-540-24651-0_24

work page doi:10.1007/978-3-540-24651-0_24 2004

[5] [5]

Mathematical Logic Quarterly 45(4), pp

Radim Bˆ elohl´ avek (1999):Fuzzy Galois Connections . Mathematical Logic Quarterly 45(4), pp. 497–504, doi:10.1002/malq.19990450408

work page doi:10.1002/malq.19990450408 1999

[6] [6]

Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2023): Labelled Calculi for the Logics of Rough Concepts

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, K rishna B. Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2023): Labelled Calculi for the Logics of Rough Concepts . Logic and Its Applications , pp. 172–188, doi: 10.1007/978-3-031-26689-8_13

work page doi:10.1007/978-3-031-26689-8_13 2023

[7] [7]

In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer Nature Switzerland Cham, pp

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, K rishna B Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2023): Non-distributive description logic . In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer Nature Switzerland Cham, pp. 49–69, doi:10.1007/978-3-031-43513-3_4

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

[8] [8]

Non-distributive description logic

Ineke van der Berg, Andrea De Domenico, Giuseppe Greco, K rishna B. Manoorkar, Alessandra Palmigiano & Mattia Panettiere (2024): Non-distributive description logic. arXiv: 2307.09561. Y . Ding, K. Manoorkar 59

work page Pith review arXiv 2024