Strong Faithfulness for ELH Ontology Embeddings

Lacerda, Victor; Ozaki, Ana; Guimarães, Ricardo

doi:10.4230/TGDK.2.3.2

Strong Faithfulness for $\mathcal{ELH}$ Ontology Embeddings

Victor Lacerda

University of Bergen, Norway Ana Ozaki

University of Oslo, Norway
University of Bergen, Norway Ricardo Guimarães

Zivid AS, Norway

Abstract

Ontology embedding methods are powerful approaches to represent and reason over structured knowledge in various domains. One advantage of ontology embeddings over knowledge graph embeddings is their ability to capture and impose an underlying schema to which the model must conform. Despite advances, most current approaches do not guarantee that the resulting embedding respects the axioms the ontology entails. In this work, we formally prove that normalized ${\cal ELH}$ has the strong faithfulness property on convex geometric models, which means that there is an embedding that precisely captures the original ontology. We present a region-based geometric model for embedding normalized ${\cal ELH}$ ontologies into a continuous vector space. To prove strong faithfulness, our construction takes advantage of the fact that normalized ${\cal ELH}$ has a finite canonical model. We first prove the statement assuming (possibly) non-convex regions, allowing us to keep the required dimensions low. Then, we impose convexity on the regions and show the property still holds. Finally, we consider reasoning tasks on geometric models and analyze the complexity in the class of convex geometric models used for proving strong faithfulness.

Keywords and phrases:

Knowledge Graph Embeddings, Ontologies, Description Logic

Funding:

Victor Lacerda: Lacerda is supported by the NFR project “Learning Description Logic Ontologies”, grant number 316022, led by Ozaki.

Ana Ozaki: Ozaki is supported by the NFR project “Learning Description Logic Ontologies”, grant number 316022.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Description logics

Supplementary Material:

The authors declare that this article involves no relevant supplemental resources.

DOI:

10.4230/TGDK.2.3.2

Received:

2024-04-24

Accepted:

2024-10-23

Published:

2024-12-18

Part Of:

TGDK, Volume 2, Issue 3

Journal and Publisher:

Transactions on Graph Data and Knowledge, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Knowledge Graphs (KGs) are a popular method for representing knowledge using triples of the form (subject, predicate, object), called facts.

Although public KGs, such as Wikidata [25], contain a large number of facts, they are incomplete. This has sparked interest in using machine learning methods to suggest plausible facts to add to the KG based on patterns found in the data. Such methods are based on knowledge graph embedding (KGE) techniques, which aim to create representations of KGs in vector spaces. By representing individuals in a vector space, these individuals can be ranked by how similar they are to each other, based on a similarity metric.

Their proximity in a vector space may be indicative of semantic similarity, which can be leveraged to discover new facts: if two individuals are close to each other in the embedding space, it is likely that they share a pattern of relations to other individuals. These patterns of relations can indicate of assertions not explicitly stated in the source knowledge graph.

Many attempts have been made to learn representations of knowledge graphs for use in downstream tasks [8]. These methods have traditionally focused only on embedding triples (facts), ignoring the conceptual knowledge about the domain expressed using logical operators. The former corresponds to the “Assertion Box”(ABox) of the ontology, while the latter corresponds to the “Terminological Box” (TBox) part of a knowledge base, with both being quite established notions in the fields of Description Logic and Semantic Web [2, 12]. Embeddings that consider both types of logically expressed knowledge are a more recent phenomenon (see Section 2), and we refer to them as ontology embeddings, where the ontology can have both an ABox and a TBox. Ontology embeddings offer advantages over traditional KGEs as they exploit the semantic relationships between concepts and roles. This enables ontology embeddings to better capture rich and nuanced relationships between concepts, making them good candidates for tasks requiring fine-grained reasoning, such as hierarchical reasoning and logical inference.

One question that arises in the study of ontology embeddings is the following: how similar to the source ontology are the generated embeddings? Being more strict, if we fix a semantics in order to interpret the generated embeddings, are they guaranteed to precisely represent the meaning of the source ontology and its entailments (of particular interest, the TBox entailments)? This property is called the strong faithfulness property [20] and, so far, no previous work for $\mathcal{EL}$ ontology embeddings has attempted to prove the property holds for their embedding method. Moreover, the existence of embedding models satisfying this property for the $\mathcal{ELH}$ language has not been formally proven. Given that ontologies languages in the $\mathcal{EL}$ family have received most of the attention by the existing literature on ontology embeddings [22, 23, 1, 26, 14], this is a significant gap which we investigate in this work.

Contribution

We investigate whether ${\cal ELH}$ has the strong faithfulness property over convex geometric models. We first prove the statement for embeddings in low dimensions, considering a region-based representation for (possibly) non-convex regions (Section 4). Also, we prove that the same property does not hold when we consider convex regions and only $1$ dimension. We then investigate strong faithfulness on convex geometric models with more dimensions (Section 5). This result contributes to the landscape of properties for embedding methods based on geometric models [5, Proposition 11] and it provides the foundation of the implementation of FaithEL [16]. We do so including embeddings for role inclusions, a problem that has not been well studied in the ${\cal ELH}$ ontology embedding literature. We also consider model checking in convex geometric models, a topic that has not been covered in previous works (Section 6).

2 Ontology Embeddings

Various methods for embedding ontologies have been proposed, with ontologies in the $\mathcal{EL}$ family being their primary targets. $\mathcal{EL}$ is a simple yet powerful language.

These embedding methods are region-based, that is, they map concepts to regions and entities to vectors (in some cases, entities are transformed into nominals and also embedded as regions), and represent roles using translations or regions within the vector space.

The precise shape of the embedding regions varies depending on the method. In EmEL [19] and ELem [15], the embeddings map concepts to $n$ -dimensional balls. One disadvantage of this approach is that the intersection between two balls is not itself a ball. Newer approaches addressing this issue such as BoxEL, Box²EL, and ELBE [26, 14, 23], starting with BoxE [1], represent concepts as $n$ -dimensional boxes. BoxE introduced the use of so-called “translational bumps” to capture relations between entities, an idea followed by Box²EL. Another language, ${\cal ALC}$ , has been studied under a cone semantics [20], which uses axis-aligned cones as its geometric interpretation. In the context of KGEs, $n$ -dimensional parallelograms have also been used in ExpressivE [21].

Other approaches for accommodating TBox axioms in the embeddings have also been considered. Approaching the problem from a different direction, OWL2Vec* [7] targets the DL language $\mathcal{SROIQ}$ and does not rely on regions, but uses the NLP algorithm word2vec to include lexical information (such as annotations) along with the graph structure of an OWL ontology. Another framework, TransOWL [9], uses background knowledge injection to improve link prediction for models such as TransE and TransR. Additionally, there has been an increased interest in querying KGEs, with strategies utilizing query rewriting techniques being put in place to achieve better results [13].

Although expressively powerful and well performing in tasks such as subsumption checking and link prediction, the generated embeddings often lack formal guarantees with respect to the source ontology. In the KGE literature, it is a well known that, e.g., TransE [3] is unable to model one-to-many relations (a difficulty present even in recent ontology embedding methods such as BoxEL) or symmetric relations. This has spurted a quest for more expressive models, with the intention of capturing an increasing list of relation types and properties such as composition, intersection, hierarchy of relations, among others [17, 27, 24, 21].

Expressivity is a key notion in ontology embedding methods, which often also feature these relation types and potentially other forms of constraints. For example, in Box²EL, ELem, and ELBE [14, 15, 23], axioms of the form $\exists r.C\sqsubseteq\bot$ are only approximated by $\exists r.\top\sqsubseteq\bot$ . This means that strong TBox faithfulness is not respected. Moreover, only EmEL and Box²EL [19, 14] include embeddings for role inclusions. In the case of EmEL, the axiom $r\sqsubseteq s$ also enforces $s\sqsubseteq r$ , which means it is not strongly faithful, while Box²EL has also been shown to not be strongly faithful [5].

3 Basic Notions

3.1 The Description Logic $\cal ELH$

Let $N_{C}$ , $N_{R}$ , and $N_{I}$ be countably infinite and pairwise disjoint sets of concept names, role names, and individual names, respectively. $\mathcal{ELH}$ concepts $C, D$ are built according to the syntax rule

\displaystyle C,D::=\top\>|\>\bot\>|\>A\>\>|\>(C\sqcap D)\>|\>\exists r.C

where $A\in N_{C}$ and $r\in N_{R}$ . $\mathcal{ELH}$ concept inclusions (CIs) are of the form $C\sqsubseteq D$ , role inclusions (RIs) are of the form $r\sqsubseteq s$ , $\mathcal{ELH}$ concept assertions are of the form $A(a)$ and role assertions are of the form $r(a,b)$ , where $A\in N_{C}$ , $a,b\in N_{I}$ , $r,s\in N_{R}$ , and $C$ , $D$ range over ${\cal ELH}$ concepts. Instance queries (IQs) are role assertions or of the form $C(a)$ , with $C$ being an arbitrary ${\cal ELH}$ concept. An $\mathcal{ELH}$ axiom is an $\mathcal{ELH}$ CI, an RI, or an IQ. A normalized $\mathcal{ELH}$ TBox is one that only contains CIs of the following forms:

\displaystyle A_{1}\sqcap A_{2}\sqsubseteq B,\ \exists r.A\sqsubseteq B\text{,% and }A\sqsubseteq\exists r.B

where $A_{1},A_{2},A,B\in N_{C}$ and $r\in N_{R}$ . We say that an ${\cal ELH}$ concept is in normal form if it is of the form $A$ , $\exists r.A$ , or $A\sqcap B$ , with $A,B\in N_{C}$ and $r\in N_{R}$ . Similarly, an ${\cal ELH}$ ontology is in normal form if its TBox part is a normalized ${\cal ELH}$ TBox. An IQ is in normal form if it is a role assertion or of the form $C(a)$ with $C$ being a concept in normal form. The semantics of ${\cal ELH}$ is defined classically by means of interpretations $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ , where $\Delta^{\mathcal{I}}$ is a non-empty countable set called the interpretation domain, and $\cdot^{\mathcal{I}}$ is an interpretation function mapping each concept name $A$ in $N_{C}$ to a subset $A^{\mathcal{I}}$ of $\Delta^{\mathcal{I}}$ , each role name $r$ in $N_{R}$ to a binary relation $r^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$ , and each individual name $a$ in $N_{I}$ to an element $a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$ . We extend the function $\cdot^{\mathcal{I}}$ inductively to arbitrary concepts by setting $\top^{\mathcal{I}}:=\Delta^{\mathcal{I}}$ , $\bot^{\mathcal{I}}:=\emptyset$ , and

	$\displaystyle(C\sqcap D)^{\mathcal{I}}$	$\displaystyle:=C^{\mathcal{I}}\cap D^{\mathcal{I}},\text{ and }$
	$\displaystyle(\exists r.C)^{\mathcal{I}}$	$\displaystyle:=\{d\in\Delta^{\mathcal{I}}\mid\exists e\in C^{\mathcal{I}}\text% { such that }(d,e)\in r^{\mathcal{I}}\}.$

An interpretation $\mathcal{I}$ satisfies: (1) $C\sqsubseteq D$ iff $C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$ ; (2) $r\sqsubseteq s$ iff $r^{\mathcal{I}}\subseteq s^{\mathcal{I}}$ , (3) $C(a)$ iff $a^{\mathcal{I}}$ $\in{C^{\mathcal{I}}}$ ; (4) $r(a,b)$ iff $(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$ .

An ${\cal ELH}$ TBox $\mathcal{T}$ (Terminological Box) is a finite number of ${\cal ELH}$ concept and role inclusions. An ${\cal ELH}$ ABox $\mathcal{A}$ (Assertion Box) is a finite number of ${\cal ELH}$ concept and role assertions. The union of a TBox and an ABox forms an ${\cal ELH}$ ontology. An ${\cal ELH}$ ontology $\mathcal{O}$ entails an ${\cal ELH}$ axiom $\alpha$ , in symbols $\mathcal{O}\models\alpha$ if for every interpretation $\mathcal{I}$ , we have that $\mathcal{I}\models\mathcal{O}$ implies $\mathcal{I}\models\alpha$ (we may write similarly for the CI and RI entailments of a TBox). We denote by $N_{C}(\mathcal{O}),N_{R}(\mathcal{O}),N_{I}(\mathcal{O})$ the set of concept names, role names, and individual names occurring in an ontology $\mathcal{O}$ . We may also write $N_{I}(\mathcal{A})$ for the set of individual names occurring in an ABox $\mathcal{A}$ . The signature of an ontology $\mathcal{O}$ , denoted ${\sf sig}(\mathcal{O})$ , is the union of $N_{C}(\mathcal{O}),N_{R}(\mathcal{O}),$ and $N_{I}(\mathcal{O})$ .

3.2 Geometric models

We go from the traditional model-theoretic interpretation of the ${\cal ELH}$ language to geometric interpretations, using definitions from previous works by [10] and [6]. Let $m$ be a natural number and $f\colon\mathbb{R}^{m}\times\mathbb{R}^{m}\mapsto\mathbb{R}^{2\cdot m}$ a fixed but arbitrary linear map satisfying the following:

1.

the restriction of $f$ to $\mathbb{R}^{m}\times\{0\}^{m}$ is injective;
2.

the restriction of $f$ to $\{0\}^{m}\times\mathbb{R}^{m}$ is injective;
3.

$f(\mathbb{R}^{m}\times\{0\}^{m})\cap f(\{0\}^{m}\times\mathbb{R}^{m})=\{0^{2% \cdot m}\}$ ;

where $0^{m}$ denotes the vector $(0,...,0)$ with $m$ zeros. We say that a linear map that satisfies Points 1, 2, and 3 is an isomorphism preserving linear map.

Example 1.

The concatenation function is a linear map that satisfies Points 1, 2, and 3. E.g., if we have vectors $v_{1}=(n_{1},n_{2},n_{3})$ and $v_{2}=(m_{1},m_{2},m_{3})$ then for $f$ being the concatenation function we would have $f(v_{1},v_{2})=(n_{1},n_{2},n_{3},m_{1},m_{2},m_{3})$ . Other linear maps that satisfy Points 1, 2, and 3 can be created with permutations. E.g., defining the function $f$ such that $f(v_{1},v_{2})=(n_{1},m_{1},n_{2},m_{2},n_{3},m_{3})$ .

Definition 2 (Geometric Interpretation).

Let $f$ be an isomorphism preserving linear map and $m$ a natural number. An $m$ -dimensional $f$ -geometric interpretation $\eta$ of $(N_{C},N_{R},N_{I})$ assigns to each

$\blacksquare$

$A\in N_{C}$ a region $\eta(A)\subseteq\mathbb{R}^{m}$
$\blacksquare$

$r\in N_{R}$ a region $\eta(r)\subseteq\mathbb{R}^{2\cdot m}$ , and
$\blacksquare$

$a\in N_{I}$ a vector $\eta(a)\in\mathbb{R}^{m}.$

We now extend the definition for arbitrary ${\cal ELH}$ concepts:

	$\displaystyle\eta(\bot)$	$\displaystyle:=\emptyset$
	$\displaystyle\eta(\top)$	$\displaystyle:=\mathbb{R}^{m},$
	$\displaystyle\eta(C\sqcap D)$	$\displaystyle:=\eta(C)\cap\eta(D)\text{, and }$
	$\displaystyle\eta(\exists r.C)$	$\displaystyle:=\{v\in\mathbb{R}^{m}\mid\exists u\in\eta(C)\text{ with }f(v,u)% \in\eta(r)\}.$

Intuitively, the function $f$ combines two vectors that represent a pair of elements in a classical interpretation relation. An $m$ -dimensional $f$ -geometric interpretation $\eta$ satisfies

$\blacksquare$

an ${\cal ELH}$ concept assertion $A(a)$ , if $\eta(a)\in\eta(A)$ ,
$\blacksquare$

a role assertion $r(a,b)$ , if $f(\eta(a),\eta(b))\in\eta(r)$ ,
$\blacksquare$

an ${\cal ELH}$ IQ $C(a)$ , if $\eta(a)\in\eta(C)$ ,
$\blacksquare$

an ${\cal ELH}$ CI $C\sqsubseteq D$ , if $\eta(C)\subseteq\eta(D)$ , and
$\blacksquare$

an RI $r\sqsubseteq s$ , if $\eta(r)\subseteq\eta(s)$ .

We write $\eta\models\alpha$ if $\eta$ satisfies an ${\cal ELH}$ axiom $\alpha$ . When speaking of $m$ -dimensional $f$ -geometric interpretations, we may omit $m$ -dimensional and $f$ -, as well as use the term “model” instead of “interpretation”. A geometric interpretation satisfies an ontology $\mathcal{O}$ , in symbols $\eta\models\mathcal{O}$ , if it satisfies all axioms in $\mathcal{O}$ . We say that a geometric interpretation is finite if the regions associated with concept and role names have a finite number of vectors and we only need to consider a finite number of individual names, which is the case when considering the individual names that occur in an ontology.

Motivated by the theory of conceptual spaces and findings on cognitive science [11, 28], and by previous work on ontology embeddings for quasi-chained rules [10], we consider convexity as an interesting restriction for the regions associated with concepts and relations in a geometric model.

Definition 3.

A geometric interpretation $\eta$ is convex if, for every $E\in N_{C}\cup N_{R}$ , every $v_{1},v_{2}\in\eta(E)$ and every $\lambda\in[0,1]$ , if $v_{1},v_{2}\in\eta(E)$ then $(1-\lambda)v_{1}+\lambda v_{2}\in\eta(E)$ .

Definition 4.

Let $S=\{v_{1},\ldots,v_{m}\}\subseteq\mathbb{R}^{d}$ . A vector $v$ is in the convex hull $S^{*}$ of $S$ iff there exist $v_{1},\ldots,v_{n}\in S$ and scalars $\lambda_{1},\lambda_{2},...,\lambda_{n}\in\mathbb{R}$ such that

v=\sum_{i=1}^{n}\lambda_{i}v_{i}=\lambda_{1}v_{1}+\lambda_{2}v_{2}+...+\lambda% _{n}v_{n},

where $\lambda_{i}\geq 0$ , for $i=1,\ldots,n$ , and $\sum_{i=1}^{n}\lambda_{i}=1$ .

Apropos of convexity, we highlight and prove some of its properties used later in our results.

Proposition 5.

For finite $S_{1},S_{2}\subseteq\mathbb{R}^{d}$ , where $d$ is an arbitrary dimension, we have that $S_{1}\subseteq S_{2}$ implies $S_{1}^{\ast}\subseteq S_{2}^{\ast}$ .

In the following, whenever we say a vector is binary, we mean that its values in each dimension can only be $0$ or $1$ .

Theorem 6.

Let $S\subseteq\{0,1\}^{d}$ where $d$ is an arbitrary dimension. For any $n\in\mathbb{N}$ , for any $v=\sum_{i=1}^{n}\lambda_{i}v_{i}$ , such that $v_{i}\in S$ , if $v\in S^{*}\setminus S$ then $v$ is non-binary.

Corollary 7.

If $v$ is binary and $v\in S^{\ast}$ then $v\in S$ .

Finally, we define strong faithfulness based on the work by [20].

Definition 8 (Strong Faithfulness).

Let $\mathcal{O}$ be a satisfiable ontology (or any other representation allowing the distinction between IQs and TBox axioms). Given an $m$ -dimensional $f$ -geometric interpretation $\eta$ , we say that:

$\blacksquare$

$\eta$ is a strongly concept-faithful model of $\mathcal{O}$ iff, for every concept $C$ and individual name $b$ , if $\eta(b)\in\eta(C)$ then $\mathcal{O}\models C(b)$ ;
$\blacksquare$

$\eta$ is a strongly IQ faithful model of $\mathcal{O}$ iff it is strongly concept-faithful and for each role $r$ and individual names $a, b$ : if $f(\eta(a),\eta(b))\in\eta(r)$ , then $\mathcal{O}\models r(a,b)$ ;
$\blacksquare$

$\eta$ is a strongly TBox-faithful model of $\mathcal{O}$ iff for all TBox axioms $\tau$ : if $\eta\models\tau$ , then $\mathcal{O}\models\tau$ .

Example 9.

Let $\mathcal{O}$ be an ontology given by $\mathcal{T}\cup\mathcal{A}$ with $\mathcal{T}=\{A\sqsubseteq B\}$ and $\mathcal{A}=\{A(a),B(b)\}$ . Let $\eta_{\mathcal{I}}$ be a (non-convex) geometric interpretation of $\mathcal{O}$ in $\mathbb{R}$ , where $\eta_{\mathcal{I}}(A)=\{0,1,2\}$ , $\eta_{\mathcal{I}}(B)=\{0,1,2,3\}$ , $\eta_{\mathcal{I}}(a)=2$ , and $\eta_{\mathcal{I}}(b)=3$ . Note that $\mathcal{O}\models A(a)$ and $\mathcal{O}\models B(b)$ , and by definition $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(A)$ , $\eta_{\mathcal{I}}(b)\in\eta_{\mathcal{I}}(B)$ . Also, $\mathcal{O}\models A\sqsubseteq B$ and $\eta_{\mathcal{I}}(A)\subseteq\eta_{\mathcal{I}}(B)$ . So one can see that $\eta_{\mathcal{I}}$ is both a strongly concept and TBox-faithful model of $\mathcal{O}$ . If we let $\eta_{\mathcal{I}}^{\prime}$ be a geometric interpretation such that $\eta_{\mathcal{I}}^{\prime}(A)=\{0,1,2,3\}=\eta_{\mathcal{I}}(B)$ , we now have that $\eta_{\mathcal{I}}^{\prime}(b)\in\eta_{\mathcal{I}}^{\prime}(A)$ , which means $\eta_{\mathcal{I}}^{\prime}$ is not a strongly concept-faithful model of $\mathcal{O}$ (since $\mathcal{O}\not\models A(b)$ ), and we have that $\eta_{\mathcal{I}}^{\prime}(B)\subseteq\eta_{\mathcal{I}}^{\prime}(A)$ , which means it is not a strongly TBox-faithful model of $\mathcal{O}$ (since $\mathcal{O}\not\models B\sqsubseteq A$ ).

We say that an ontology language has the strong faithfulness property over a class of geometric interpretations $\mathcal{C}$ if for every satisfiable ontology $\mathcal{O}$ in this language there is a geometric interpretation in $\mathcal{C}$ that is both a strongly IQ faithful and a strongly TBox faithful model of $\mathcal{O}$ .

The range of concepts, roles, and individual names in Definition 8 varies depending on the language and setting studied. We omit the notion of weak faithfulness by [20] as it does not apply for ${\cal ELH}$ since ontologies in this language are always satisfiable (there is no negation). The “if-then” statements in Definition 8 become “if and only if” when $\eta$ satisfies the ontology. Intuitively, strong faithfulness expresses how similar the generated embedding is to the original ontology.

We observe that strong faithfulness with respect to the TBox component of the ontology is extremely desirable: it guarantees that concept and role inclusions are also enforced when coupled with a geometric interpretation in the embedding space. On the other hand, strong IQ faithfulness is not a desirable property for learned embeddings. Although this might seem counter-intuitive at first, it is a reasonable statement: an embedding that is strongly IQ faithful is unsuitable for link prediction, as the only assertions that hold in the embedding are those that already hold in the original ontology. This means that no new facts are truly discovered by the model. Here we prove both strong TBox and IQ faithfulness for ${\cal ELH}$ for theoretical reasons.

Finally, observe that an embedding model that is both strongly TBox and IQ faithful must have the same TBox and IQ consequences as the original ontology. This is a stronger requirement than establishing that an embedding model for an ontology $\mathcal{O}$ (within a method) exist if and only if a classical model for $\mathcal{O}$ exists, which is a property of sound and complete embedding methods [5].

4 Strong Faithfulness

In this section we prove initial results about strong faithfulness for ${\cal ELH}$ . In particular, we prove that ${\cal ELH}$ has the strong faithfulness property over $m$ -dimensional $f$ -geometric interpretations for any $m\geq 1$ but this is not the case if we require that regions in the geometric interpretations are convex. We first introduce a mapping from classical interpretation to (possibly) non-convex geometric interpretations and then use it with the notion of canonical model to establish strong faithfulness for ${\cal ELH}$ .

Definition 10.

Let $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ be a classical ${\cal ELH}$ interpretation, and we assume without loss of generality, since $\Delta^{\mathcal{I}}$ is non-empty and countable, that $\Delta^{\mathcal{I}}$ is a (possibly infinite) interval in $\mathbb{N}$ starting on $0$ . Let $\bar{\mu}\colon{\Delta^{\mathcal{I}}\mapsto{\mathbb{R}^{1}}}$ be a mapping from our classical interpretation domain to a vector space where:

\displaystyle\bar{\mu}(d)=\begin{cases}(-\infty,-d]\cup[d,\infty),&\text{if }% \Delta^{\mathcal{I}}\text{is finite and }d=max(\Delta^{\mathcal{I}}),\\ (-d-1,-d]\cup[d,d+1),&\text{otherwise.}\end{cases}

where $d\in\mathbb{N}$ and $(-d-1,-d]$ and $[d,d+1)$ are intervals over $\mathbb{R}^{1}$ , closed on $d$ and $-d$ , and open on $d+1$ and $-d-1$ .

$\blacktriangleright$ Remark 11.

For any interpretation $\mathcal{I}$ , $\bar{\mu}$ covers the real line, that is, $\bigcup_{d\in\Delta^{\mathcal{I}}}\bar{\mu}(d)=\mathbb{R}^{1}$ .

Definition 12.

We call $\bar{\eta}_{\mathcal{I}}$ the geometric interpretation of $\mathcal{I}$ and define it as follows. Let $\mathcal{I}$ be a classical ${\cal ELH}$ interpretation. The geometric interpretation of $\mathcal{I}$ , denoted $\bar{\eta}_{\mathcal{I}}$ , is defined as:

	$\displaystyle\bar{\eta}_{\mathcal{I}}(a)$	$\displaystyle:=d\text{, such that }d=a^{\mathcal{I}}\text{, for all }a\in N_{I},$
	$\displaystyle\bar{\eta}_{\mathcal{I}}(A)$	$\displaystyle:=\{v\in\bar{\mu}(d)\mid d\in A^{\mathcal{I}}\}\text{, for all }A% \in N_{C},\text{ and }$
	$\displaystyle\bar{\eta}_{\mathcal{I}}(r)$	$\displaystyle:=\{f(v,e)\mid v\in\bar{\mu}(d)\text{ for }(d,e)\in r^{\mathcal{I% }}\}\text{, for all }r\in N_{R}.$

Figure 1: A partial visualization (showing only the positive section of the real line) of a geometric interpretation

\bar{\eta}_{\mathcal{I}}

where elements

d_{0}\ldots d_{3}

are mapped to their respective intervals, and where

\bar{\mu}(d_{0}),\bar{\mu}(d_{2}),\bar{\mu}(d_{3})\in\bar{\eta}_{\mathcal{I}}(A)

and

\bar{\mu}(d_{2})\in\bar{\eta}_{\mathcal{I}}(B)

.

In Figure 1, we illustrate with an example the mapping in Definition 12. We now show that for (possibly) non-convex geometric models, a classical interpretation $\mathcal{I}$ models arbitrary IQs and arbitrary TBox axioms if and only if their geometrical interpretation $\bar{\eta}_{\mathcal{I}}$ also models them.

Theorem 13.

For all ${\cal ELH}$ axioms $\alpha$ , $\mathcal{I}\models\alpha$ iff $\bar{\eta}_{\mathcal{I}}\models\alpha$ .

We now provide a definition of canonical model for ${\cal ELH}$ ontologies inspired by a standard chase procedure. In our definition, we use a tree shaped interpretation $\mathcal{I}_{D}$ of an ${\cal ELH}$ concept $D$ , with the root denoted $\rho_{D}$ . This is defined inductively. For $D$ a concept name $A\in N_{C}$ we define $\mathcal{I}_{A}$ as the interpretation with $\Delta^{\mathcal{I}_{A}}:=\{\rho_{A}\}$ , $A^{\mathcal{I}_{A}}:=\{\rho_{A}\}$ , and all other concept and role names interpreted as the empty set. For $D=\exists r.C$ , we define $\mathcal{I}_{D}$ as the interpretation with $\Delta^{\mathcal{I}_{D}}:=\{\rho_{D}\}\cup\Delta^{\mathcal{I}_{C}}$ , all concept and role name interpretations are as for $\mathcal{I}_{C}$ except that we add $(\rho_{D},\rho_{C})$ to $r^{\mathcal{I}_{D}}$ and assume $\rho_{D}$ is fresh (i.e., it is not in $\Delta^{\mathcal{I}_{C}}$ ). Finally, for $D=C_{1}\sqcap C_{2}$ we define $\Delta^{\mathcal{I}_{D}}:=\Delta^{\mathcal{I}_{C_{1}}}\cup(\Delta^{\mathcal{I}% _{C_{2}}}\setminus\{\rho_{C_{2}}\})$ , assuming $\Delta^{\mathcal{I}_{C_{1}}}$ and $\Delta^{\mathcal{I}_{C_{2}}}$ are disjoint, and with all concept and role name interpretations as in $\mathcal{I}_{C_{1}}$ and $\mathcal{I}_{C_{2}}$ , except that we connect $\rho_{C_{1}}$ with the elements of $\Delta^{\mathcal{I}_{C_{2}}}$ in the same way as $\rho_{C_{2}}$ is connected. That is, we identify $\rho_{C_{1}}$ with the root $\rho_{C_{2}}$ of $\mathcal{I}_{D_{2}}$ .

Definition 14.

The canonical model ${\bar{\mathcal{I}}_{\mathcal{O}}}$ of a satisfiable ${\cal ELH}$ ontology $\mathcal{O}$ is defined as the union of a sequence of interpretations $\mathcal{I}_{0},\mathcal{I}_{1},\ldots$ , where $\mathcal{I}_{0}$ is defined as:

	$\displaystyle\Delta^{\mathcal{I}_{0}}$	$\displaystyle:=\{a\mid a\in N_{I}(\mathcal{A})\},$
	$\displaystyle A^{\mathcal{I}_{0}}$	$\displaystyle:=\{a\mid A(a)\in\mathcal{A}\}\text{ for all }A\in N_{C},\text{ % and }$
	$\displaystyle r^{\mathcal{I}_{0}}$	$\displaystyle:=\{(a,b)\mid r(a,b)\in\mathcal{A}\},\text{ for all }r\in N_{R}.$

Suppose $\mathcal{I}_{n}$ is defined. We define $\mathcal{I}_{n+1}$ by choosing a CI or an RI in $\mathcal{O}$ and applying one of the following rules:

$\blacksquare$

if $C\sqsubseteq D\in\mathcal{O}$ and $d\in C^{\mathcal{I}_{n}}\setminus D^{\mathcal{I}_{n}}$ then define $\mathcal{I}_{n+1}$ as the result of adding to $\mathcal{I}_{n}$ a copy of the tree shaped interpretation $\mathcal{I}_{D}$ and identifying $d$ with the root of $\mathcal{I}_{D}$ (assume that the elements in $\Delta^{\mathcal{I}_{D}}$ are fresh, that is, $\Delta^{\mathcal{I}_{D}}\cap\Delta^{\mathcal{I}_{n}}=\emptyset$ );
$\blacksquare$

if $r\sqsubseteq s\in\mathcal{O}$ and $(d,e)\in r^{\mathcal{I}_{n}}\setminus s^{\mathcal{I}_{n}}$ then set $\mathcal{I}_{n+1}$ as the result of adding $(d,e)$ to $s^{\mathcal{I}_{n}}$ .

We assume the choice of CIs and RIs and corresponding rule above to be fair, i.e., if a CI or RI applies at a certain place, it will eventually be applied there.

Theorem 15.

Let $\mathcal{O}$ be a satisfiable ${\cal ELH}$ ontology and let ${\bar{\mathcal{I}}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (Definition 14). Then,

$\blacksquare$

for all ${\cal ELH}$ IQs and CIs $\alpha$ over ${\sf sig}(\mathcal{O})$ , ${\bar{\mathcal{I}}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ ; and
$\blacksquare$

for all RIs $\alpha$ over ${\sf sig}(\mathcal{O})$ , ${\bar{\mathcal{I}}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ .

We are now ready to state our theorem combining the results of Theorems 13 and 15 and the notion of strong faithfulness for IQs and TBox axioms.

Theorem 16.

Let $\mathcal{O}$ be a satisfiable ${\cal ELH}$ ontology and let ${\bar{\mathcal{I}}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (see Definition 14). The $m$ -dimensional $f$ -geometric interpretation of ${\bar{\mathcal{I}}_{\mathcal{O}}}$ (see Definition 12) is a strongly IQ and TBox faithful model of $\mathcal{O}$ .

What Theorem 16 demonstrates is that the existence of canonical models for ${\cal ELH}$ allows us to connect our result relating classical and geometric interpretations to faithfulness. This property of canonical models is crucial and can potentially be extended to other description logics that also have canonical models (however, many of such logics do not have polynomial size canonical models, a property we use in the next section, so we focus on ${\cal ELH}$ in this work).

Corollary 17.

For all $m\geq 1$ and isomorphism preserving linear maps $f$ , ${\cal ELH}$ has the strong faithfulness property over $m$ -dimensional $f$ -geometric interpretations.

However, requiring that the regions of the geometric model are convex makes strong faithfulness more challenging. The next theorem hints that such models require more dimensions and a more principled approach to map ${\cal ELH}$ ontologies in a continuous vector space.

Figure 2: An illustration of the region

\eta_{\mathcal{I}}(A)\cap\eta_{\mathcal{I}}(B)

.

Theorem 18.

${\cal ELH}$ does not have the strong faithfulness property over convex $1$ -dimensional $f$ -geometric models.

Proof.

We reason by cases in order to show impossibility of the strong faithfulness property for the class of convex $1$ -dimensional $f$ -geometric model for arbitrary ${\cal ELH}$ ontologies. Let $\mathcal{O}$ be an ${\cal ELH}$ ontology, $A$ , $B$ , $C$ $\in N_{C}$ concept names, $a,b\in N_{I}$ individuals, and let $\eta(A)$ , $\eta(B)$ , $\eta(C)$ , $\eta(a)$ , and $\eta(b)$ be their corresponding geometric interpretations to $\mathbb{R}^{1}$ . Assume $\mathcal{O}\models A\sqcap B(a)$ . There are three initial cases on how to choose the interval placement of $\eta(A)$ and $\eta(B)$ :

$\blacksquare$

Null intersection: $(\eta(A)\cap\eta(B))=\emptyset$ .

If $(\eta(A)\cap\eta(B))=\emptyset$ , then either $(\eta(a)\in\eta(A)$ and $(\eta(a)\not\in\eta(B)$ , or $(\eta(a)\in\eta(B)$ and $(\eta(a)\not\in\eta(A)$ . Recall the definition of satisfiability for concept assertions. Since we assumed $\mathcal{O}\models A\sqcap B(a)$ , we would want our geometric interpretation to be such that $\eta(a)\in\eta(A)\cap\eta(B)$ , a contradiction.
$\blacksquare$

Total inclusion: $\eta(A)\subseteq\eta(B)$ and/or $\eta(B)\subseteq\eta(A)$ .

Consider an extension $\mathcal{O^{\prime}}$ of our ontology where $\mathcal{O^{\prime}}\models A(c)$ and $\mathcal{O^{\prime}}\not\models B(c)$ . If we let $\eta(A)\subseteq\eta(B)$ , it is clear that our ontology cannot be faithfully modeled, since by our assumption of total inclusion, we would have that $\eta(c)\in\eta(A)$ and $\eta(c)\in\eta(B)$ , which goes against $\mathcal{O^{\prime}}\not\models B(c)$ . The same holds for the total inclusion in the other direction, where $\eta(B)\subseteq\eta(A)$ . Therefore, we go to our last initial case to be considered.
$\blacksquare$

Partial intersection: $(\eta(A)\cap\eta(B))\not=\emptyset$ .

This is in fact the only way of faithfully giving a geometric interpretation to our concept assertion $A\sqcap B(a)$ , while still leaving room for ABox axioms such that an arbitrary element could belong to one of our classes $A$ or $B$ without necessarily belonging to both of them. Then, $\eta(A)\cap\eta(B)$ and $\eta(A)\not\subseteq\eta(B)$ nor $\eta(B)\not\subseteq\eta(A)$ .

After having forced the geometric interpretation of our two initial concepts $A$ and $B$ to partially intersect, we now show that by adding a third concept $C$ , in which $\mathcal{O}\models A\sqcap B\sqcap C(a)$ , either $\eta(A)\subset\eta(B)\cup\eta(C)$ or $\eta(B)\subset\eta(A)\cup\eta(C)$ , even though this interpretation is not included in our original ontology. We are unable to include a concept assertion $A(a)\in\mathcal{O}$ without also having that $\eta(a)\in\eta(C)$ in our geometric interpretation, or likewise for the case in which $B(a)\in\mathcal{O}$ .

Stemming from the fact that our geometric interpretation must be convex, and it is modeled in an euclidean $\mathbb{R}^{1}$ space, we can visualize our classes $A$ , $B$ , and $C$ as intervals on the real line. Assume, without loss of generality, that $\eta(A)$ is placed to the left of $\eta(B)$ (see Figure 2). Then, $C$ can only be placed either to the right of $B$ or to the left of $A$ .

By reasoning in the same way as before, we know that $\eta(C)$ must partially intersect with either $\eta(A)$ or $\eta(B)$ , so one end of the interval representing $C$ must be placed in $\eta(A)\cap\eta(B)$ , without us having that either $\eta(C)\subseteq\eta(A)$ , $\eta(C)\subseteq\eta(B)$ , $\eta(C)\subseteq\eta(A)\cap\eta(B)$ or $\eta(C)\subseteq\eta(A)\cup\eta(B)$ . This last requirement is due to the fact that we want to be able to have an ontology such that $\mathcal{O}\models C(a)$ and where $\mathcal{O}\not\models A(a)$ , $\mathcal{O}\not\models B(a)$ , or $\mathcal{O}\not\models A(a)\sqcap B(a)$ . Assuming the intersection between $\eta(A)$ and $\eta(B)\not=\emptyset$ there are three more cases to be considered:

$\blacksquare$

C is in the intersection of A and B: $\eta(C)\subseteq\eta(A)\cap\eta(B)$ (Fig. 2 (a)).

If $\eta(C)\subseteq\eta(A)\cap\eta(B)$ , it is immediately clear that by extending $\mathcal{O}$ such that $\mathcal{O}\models C(b)$ but $\mathcal{O}\not\models A(b)$ , we would end up with $\eta(b)\in\eta(C)$ . But since we assumed that $\eta(C)\subseteq\eta(A)\cap\eta(B)$ , this means that $\eta(b)\in\eta(A)$ , and therefore our geometric interpretation would model the concept assertion $A(b)$ , a contradiction.
$\blacksquare$

C goes from the intersection: $\eta(A)\cap\eta(B)$ to $\eta(A)\setminus\eta(B)$ (Fig. 2 (b)).

In this situation, we would have $\eta(C)\subseteq\eta(A)$ , and if $\mathcal{O}\models C(a)$ , we would necessarily have that $\eta(a)\in\eta(C)$ , but this means we would also have $\eta(a)\in\eta(A)$ , leading to the unwarranted consequence that $\eta\models A(a)$ . There is one last case.
$\blacksquare$

C is placed in a region such that: $\eta(C)\cap(\eta(A)\cup\eta(B))\not=\emptyset$ and $\eta(C)\setminus(\eta(A)\cup\eta(B))\not=\emptyset$ (Fig. 2 (c)).

This would mean that $\eta(B)\subseteq\eta(A)\cup\eta(C)$ , and that any concept assertion $B(a)$ would entail either $C(a)$ or $A(a)$ in our geometric interpretation, while it is not necessary that $\mathcal{O}\models A(a)$ or $\mathcal{O}\models B(a)$ . Since we are in $\mathbb{R}^{1}$ , this desired placement can happen either to the right or to the left of the number line. By assumption that $\eta(A)$ has been placed to the left of $\eta(B)$ as shown in Figure 2 and following, we have just shown that placing $\eta(C)$ to the right of $\eta(B)$ leads to a contradiction. The same reasoning applies if we choose to place it to the left of $\eta(A)$ .

There are no more cases to be considered. $\hfill\blacktriangleleft$

Figure 3: The three possible cases when there is an element in the intersection of

A, B, C

.

The problem illustrated in Theorem 18 arises even if the ontology language does not have roles (as it is the case, e.g., of Boolean ${\cal ALC}$ , investigated by [20]). It also holds if we restrict to normalized ${\cal ELH}$ . We address the problem of mapping normalized ${\cal ELH}$ ontologies to convex geometric models in the next section.

5 Strong Faithfulness on Convex Models

We prove that normalized ${\cal ELH}$ has the strong faithfulness property over a class of convex geometric models. We introduce a new mapping $\mu$ from the domain of a classical interpretation $\mathcal{I}$ to a vector space and a new geometric interpretation $\eta_{\mathcal{I}}$ based on this mapping. Our proofs now require us to fix the isomorphism preserving linear map $f$ used in the definition of geometric interpretations (Definition 2). We choose the concatenation function, denoted $\oplus$ , as done in the work by [10]. The strategy for proving strong faithfulness for normalized ${\cal ELH}$ requires us to (a) find a suitable non-convex geometric interpretation for concepts and roles, and (b) show that the convex hull of the region maintains the property intact.

Definition 19.

Let $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ be a classical ${\cal ELH}$ interpretation, and $\mathcal{O}$ an ${\cal ELH}$ ontology. We start by defining a new map $\mu\colon\Delta^{\mathcal{I}}\mapsto\mathbb{R}^{{\mathsf{d}}}$ , where ${\mathsf{d}}$ corresponds to $|N_{I}(\mathcal{O})|+|N_{C}(\mathcal{O})|+|N_{R}(\mathcal{O})|\cdot|\Delta^{% \mathcal{I}}|$ . We assume, without loss of generality, a fixed ordering in our indexing system for positions in vectors, where indices $0$ to $|N_{I}(\mathcal{O})|-1$ correspond to the indices for individual names; $|N_{I}(\mathcal{O})|$ to $k=|N_{I}(\mathcal{O})|+|N_{C}(\mathcal{O})|-1$ correspond to the indices for concept names; and $k$ to $k+(|N_{R}(\mathcal{O})|\cdot|\Delta^{\mathcal{I}}|)-1$ correspond to the indices for role names together with an element of $\Delta^{\mathcal{I}}$ . We adopt the notation $v[a]$ , $v[A]$ , and $v[r,d]$ to refer to the position in a vector $v$ corresponding to $a$ , $A$ , and $r$ together with an element $d$ , respectively (according to our indexing system). For example, $v{[a]=0}$ means that the value at the index corresponding to the individual name $a$ is $0$ . A vector is binary iff $v\in\{0,1\}^{{\mathsf{d}}}$ . We now define $\mu$ using binary vectors. For all $d\in\Delta^{\mathcal{I}}$ , $a\in N_{I}$ , $A\in N_{C}$ and $r\in N_{R}$ :

$\blacksquare$

$\mu(d){[a]=1}$ if $d=a^{\mathcal{I}}$ , otherwise $\mu(d){[a]}=0$ ,
$\blacksquare$

$\mu(d){[A]=1}$ if $d\in A^{\mathcal{I}}$ , otherwise $\mu(d){[A]=0}$ , and
$\blacksquare$

$\mu(d){[r,e]=1}$ if $(d,e)\in r^{\mathcal{I}}$ , otherwise $\mu(d){[r,e]=0}$ .

Figure 4: A mapping to the binary vector

\mu(d)

when

d\in\Delta^{\mathcal{I}}

, where

d\in a_{0}^{\mathcal{I}}

,

d\in A_{0}^{\mathcal{I}}

and

(d,d_{0})\in r^{\mathcal{I}}_{0}

.

Figure 4 illustrates a possible mapping for element $d\in\Delta^{\mathcal{I}}$ , where $d\in a_{0}^{\mathcal{I}}$ , $d\in A_{0}^{\mathcal{I}}$ and $(d,d_{0})\in r^{\mathcal{I}}_{0}$ .

Example 20.

Let $\mathcal{O}$ be an ontology such as in Example 9, with $\mathcal{T}=\{A\sqsubseteq B\}$ , $\mathcal{A}$ being extended to $\mathcal{A}^{\prime}=\{A(a),B(b),r(a,b)\}$ . Let $\mathcal{I}$ be an interpretation such that $\Delta^{\mathcal{I}}=\{d,e\}$ , with $a^{\mathcal{I}}=d$ , $b^{\mathcal{I}}=e$ , $r^{\mathcal{I}}=\{(d,e)\}$ , $A^{\mathcal{I}}=\{d\}$ , and $B^{\mathcal{I}}=\{d,e\}$ . In this case, $\mu:\Delta^{\mathcal{I}}\mapsto\mathbb{R}^{6}$ , with $|N_{I}(\mathcal{O})|=2$ (corresponding to $a$ and $b$ ), $|N_{C}(\mathcal{O})|=2$ (corresponding to $A$ and $B$ ), and $|N_{R}(\mathcal{O})|\cdot|\Delta^{\mathcal{I}}|=2$ corresponding to $r$ , $d$ , and $e$ . Assume our ordering in the definition holds, and assume further that the names in the signature of $\mathcal{O}$ are ordered alphabetically. We have that the six dimensions correspond to, respectively: $a,b,A,B,[r,d],[r,e]$ . By applying the mapping to the elements of $\Delta^{\mathcal{I}}$ , we get the vectors $\mu(d)=(1,0,1,1,0,1)$ and $\mu(e)=(0,1,0,1,0,0)$ .

We now introduce a definition for (possibly) non-convex geometric interpretations, in line with the mapping $\mu$ above.

Definition 21.

Let $\mathcal{I}$ be a classical $\mathcal{ELH}$ interpretation. The geometric interpretation of $\mathcal{I}$ , denoted $\eta_{\mathcal{I}}$ , is defined as:

	$\displaystyle\eta_{\mathcal{I}}(a)$	$\displaystyle:=\mu(a^{\mathcal{I}})\text{, for all }a\in N_{I},$
	$\displaystyle\eta_{\mathcal{I}}(A)$	$\displaystyle:=\{\mu(d)\mid\mu(d){[A]=1},d\in\Delta^{\mathcal{I}}\}\text{, for% all }A\in N_{C},$
	$\displaystyle\eta_{\mathcal{I}}(r)$	$\displaystyle:=\{\mu(d)\oplus\mu(e)\mid\mu(d){[r,e]=1},d,e\in\Delta^{\mathcal{% I}}\}\text{, for all }r\in N_{R}.$

We provide two examples, one covering both concept and role assertions, and one (which can be represented graphically), covering only concept assertions.

Example 22.

Let $\mathcal{O}$ , $\mathcal{I}$ be as in Example 20. Then, the geometric interpretation $\eta_{\mathcal{I}}$ of $\mathcal{I}$ is as: $\eta_{\mathcal{I}}(a)=\mu(d)$ , $\eta_{\mathcal{I}}(b)=\mu(e)$ , $\eta_{\mathcal{I}}(A)=\{\mu(d)\}$ , $\eta_{\mathcal{I}}(B)=\{\mu(d),\mu(e)\},\eta_{\mathcal{I}}(r)=\{\mu(d)\oplus% \mu(e)\}$ . We remark that this is a strongly faithful TBox embedding.

An intuitive way of thinking about our definition $\mu$ is that it maps domain elements to a subset of the vertex set of the ${\mathsf{d}}$ -dimensional unit hypercube (see Example 23).

Figure 5: A mapping of

\mu(d)

and

\mu(e)

according to interpretation

\mathcal{I}

. The axes colored in red, blue, and green correspond to the dimensions associated with

a

,

A

, and

B

, respectively.

Example 23.

Consider $A,B\in N_{C}$ and $a\in N_{I}$ . Let $\mathcal{I}$ be an interpretation with $d,e\in\Delta^{\mathcal{I}}$ such that $d=a^{\mathcal{I}}$ , $d\in A^{\mathcal{I}}$ , and $e\in A^{\mathcal{I}}\cap B^{\mathcal{I}}$ . We illustrate $\mu(d)$ and $\mu(e)$ in Figure 5. In symbols, $\mu(d)[a]=1$ , $\mu(d)[A]=1$ , and $\mu(d)[B]=0$ , while $\mu(e)[a]=0$ , $\mu(e)[A]=1$ , and $\mu(e)[B]=1$ .

Before proving strong faithfulness with convex geometric models, we show that $\eta_{\mathcal{I}}$ preserves the axioms that hold in the original interpretation $\mathcal{I}$ . It is possible for two elements $d,e\in\Delta^{\mathcal{I}}$ to be mapped to the same vector $v$ as a result of our mapping $\mu$ . This may happen when $d, e$ $\not\in\{a^{\mathcal{I}}\mid a\in N_{I}\}$ but it does hinder our results.

Proposition 24.

If $\mu(d)=\mu(e)$ , then $d\in C^{\mathcal{I}}$ iff $e\in C^{\mathcal{I}}$ .

We use a similar strategy as before to prove our result.

Theorem 25.

For all ${\cal ELH}$ axioms $\alpha$ , $\mathcal{I}\models\alpha$ iff $\eta_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ .

Since the definition of $\eta_{\mathcal{I}}$ uses vectors in a dimensional space that depends on the size of $\Delta^{\mathcal{I}}$ and $\mathcal{O}$ , we need the canonical models to be finite. Therefore, we employ finite canonical models for normalized $\mathcal{ELH}$ because canonical models for arbitrary ${\cal ELH}$ CIs are not guaranteed to be finite. Our definition of canonical model is a non-trivial adaptation of other definitions found in the literature (e.g., [4, 18]).

Let $\mathcal{A}$ be an $\mathcal{ELH}$ ABox, $\mathcal{T}$ a normalized $\mathcal{ELH}$ TBox, and $\mathcal{O}:=\mathcal{A}\cup\mathcal{T}$ . We first define:

	$\displaystyle\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$	$\displaystyle:=\{c_{A}\,\|\,A\in N_{C}(\mathcal{O})\cup\{\top\}\}\text{ and }$
	$\displaystyle\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$	$\displaystyle:=\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}\cup\{c_{A\sqcap B}\,\|\,A% ,B\in N_{C}(\mathcal{O})\}\ \cup\ \{c_{\exists r.B}\,\|\,r\in N_{R}(\mathcal{O}% ),B\in N_{C}(\mathcal{O})\cup\{\top\}\}.$

Definition 26.

The canonical model $\mathcal{I}_{\mathcal{O}}$ of $\mathcal{O}$ is defined as

	$\displaystyle\Delta^{\mathcal{I}_{\mathcal{O}}}$	$\displaystyle:=N_{I}(\mathcal{A})\cup\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+},% \quad\quad a^{\mathcal{I}_{\mathcal{O}}}:=a,$
	$\displaystyle A^{\mathcal{I}_{\mathcal{O}}}$	$\displaystyle:=\{a\in N_{I}(\mathcal{A})\,\|\,\mathcal{O}\models A(a)\}\ \cup\ % \{c_{D}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\,\|\,\mathcal{T}\models D% \sqsubseteq A\}\text{, and }$
	$\displaystyle r^{\mathcal{I}_{\mathcal{O}}}$	$\displaystyle:=\{(a,b)\in N_{I}(\mathcal{A})\times N_{I}(\mathcal{A})\,\|\,% \mathcal{O}\models r(a,b)\}\ \cup$
		$\displaystyle\{(a,c_{B})\in N_{I}(\mathcal{A})\times\Delta^{\mathcal{I}_{% \mathcal{O}}}_{u}\,\|\,\mathcal{O}\models\exists r.B(a)\}\cup\{(c_{\exists s.B}% ,c_{B})\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\times\Delta^{\mathcal{I}_{% \mathcal{O}}}_{u}\,\|\,\mathcal{T}\models s\sqsubseteq r\}$
		$\displaystyle\cup\{(c_{D},c_{B})\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}% \times\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}\,\|\,\mathcal{T}\models D% \sqsubseteq A,\ \mathcal{T}\models A\sqsubseteq\exists r.B,\text{ for some }A% \in N_{C}(\mathcal{O})\},$

for all $a\in N_{I}$ , $A\in N_{C}$ , and $r\in N_{R}$ .

The following holds for the canonical model just defined.

Theorem 27.

Let $\mathcal{O}$ be a normalized ${\cal ELH}$ ontology. The following holds

$\blacksquare$

for all ${\cal ELH}$ IQs and CIs $\alpha$ in normal form over ${\sf sig}(\mathcal{O})$ , ${\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ ; and
$\blacksquare$

for all RIs $\alpha$ over ${\sf sig}(\mathcal{O})$ , ${\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ .

The main difference between our definition and other canonical model definitions in the literature is related to our purposes of proving strong faithfulness, as we discuss in Section 5. We require the CIs and RIs (in normal form and in ${\sf sig}(\mathcal{O})$ ) that are entailed by the ontology are exactly those that hold in the canonical model.

Theorem 28.

Let $\mathcal{O}$ be an ${\cal ELH}$ ontology and let ${\mathcal{I}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (Definition 26). The ${\mathsf{d}}$ -dimensional (possibly non-convex) $\oplus$ -geometric interpretation $\eta_{{\mathcal{I}_{\mathcal{O}}}}$ of ${\mathcal{I}_{\mathcal{O}}}$ is a strongly and IQ and TBox faithful model of $\mathcal{O}$ .

We now proceed with the main theorems of this section. Note that the dimensionality of the image domain of $\mu$ can be much higher than the one for $\bar{\mu}$ in Section 4 (which can be as low as just $1$ , see Corollary 17). We use the results until now as intermediate steps to bridge the gap between classical and convex geometric interpretations. In our construction of convex geometric interpretations, the vectors mapped by $\mu$ and the regions given by the non-convex geometric interpretation $\eta_{\mathcal{I}}$ are the anchor points for the convex closure of these sets. We introduce the notion of the convex hull of a geometric interpretation $\eta_{\mathcal{I}}$ using Definition 4.

Definition 29.

We denote by $\eta_{\mathcal{I}}^{*}$ the convex hull of the geometric interpretation $\eta_{\mathcal{I}}$ and define $\eta_{\mathcal{I}}^{*}$ as follows:

	$\displaystyle\eta_{\mathcal{I}}^{*}(a)$	$\displaystyle:=\mu(a^{\mathcal{I}})\text{, for all }a\in N_{I};$
	$\displaystyle\eta_{\mathcal{I}}^{*}(A)$	$\displaystyle:=\{\mu(d)\mid d\in A^{\mathcal{I}}\}^{*}\text{, for all }A\in N_% {C};\text{ and }$
	$\displaystyle\eta_{\mathcal{I}}^{*}(r)$	$\displaystyle:=\{\mu(d)\oplus\mu(e)\mid(d,e)\in r^{\mathcal{I}}\}^{*}\text{, % for all }r\in N_{R}.$

$\blacktriangleright$ Remark 30.

In Definition 29, $\eta_{\mathcal{I}}^{*}(a)=\eta_{\mathcal{I}}(a)$ for all $a\in N_{I}$ . We include the star symbol in the notation to make it clear that we are referring to the geometric interpretation of individual names in the context of convex regions for concepts and roles.

Theorem 31.

Let $\eta_{\mathcal{I}}$ be a geometric interpretation as in Definition 21. If $\alpha$ is an ${\cal ELH}$ CI, an ${\cal ELH}$ RI, or an ${\cal ELH}$ IQ in normal form then $\eta_{\mathcal{I}}\models\alpha$ iff $\eta_{\mathcal{I}}^{*}\models\alpha$ .

We are now ready to consider strong IQ and TBox faithfulness for convex regions.

Theorem 32.

Let $\mathcal{O}$ be a normalized ${\cal ELH}$ ontology and let ${\mathcal{I}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (Definition 26). The ${\mathsf{d}}$ -dimensional convex $\oplus$ -geometric interpretation of ${\mathcal{I}_{\mathcal{O}}}$ (Definition 29) is a strongly IQ and TBox faithful model of $\mathcal{O}$ .

We now state a corollary analogous to Corollary 17, though here we cannot state it for all classes of $m$ -dimensional $f$ -geometric interpretations (we know by Theorem 18 that this is impossible for any class of $1$ -dimensional geometric interpretations). We omit “ $m$ -dimensional” in Corollary 33 to indicate that this holds for the larger class containing geometric interpretations with an arbitrary number of dimensions (necessary to cover the whole language).

Corollary 33.

Normalized ${\cal ELH}$ has the strong faithfulness property over $\oplus$ -geometric interpretations.

$\blacktriangleright$ Remark 34 (Number of parameters).

The final number of parameters for the convex geometric interpretation $\eta_{\mathcal{I}_{\mathcal{O}}}$ of the canonical model ${\mathcal{I}_{\mathcal{O}}}$ built on ontology $\mathcal{O}$ is, thus: $O({\mathsf{d}}\cdot n)$ where ${\mathsf{d}}$ is the embedding dimension given by map $\mu$ (Definition 19), and $n=|\Delta^{\mathcal{I}_{\mathcal{O}}}|$ .

6 Model Checking on Geometric Models

Here we study upper bounds for the complexity of model checking problems using convex geometric models as those defined in Definition 29 and normalized ${\cal ELH}$ axioms. The results and algorithms in this section are underpinned by Theorem 31, which allow us to use $\eta_{\mathcal{I}}$ instead of $\eta_{\mathcal{I}}^{*}$ for model checking purposes. The advantage of using $\eta_{\mathcal{I}}$ instead of $\eta_{\mathcal{I}}^{*}$ is that the algorithms need to inspect only finitely many elements in the extension of each concept and each role, as long as the original interpretation $\mathcal{I}$ has finite domain (and we only need to consider a finite number of concept, role, and individual names). For example, let $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ with $\Delta^{\mathcal{I}}$ finite. If $A\in{\sf N_{C}}$ then $\eta_{\mathcal{I}}^{*}(A)$ can have infinitely many elements, while $\eta_{\mathcal{I}}(A)$ will have at most ${|\Delta^{\mathcal{I}}|}$ elements (by Definition 21). Before presenting the algorithms, we discuss some assumptions that facilitate our analysis:

1.

indexing vectors and comparing primitive types use constant time;
2.

accessing the extension of an individual, concept, or role name in $\eta_{\mathcal{I}}$ takes constant time;
3.

iterating over $\eta_{\mathcal{I}}(A)$ (and also $\eta_{\mathcal{I}}(r)$ ) consumes time $O({|\Delta^{\mathcal{I}}|})$ ( $O({{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ ) for all $A\in{\sf N_{C}}$ ( $r\in{\sf N_{R}}$ ); and
4.

if $A\in{\sf N_{C}}$ ( $r\in{\sf N_{R}}$ ), testing if $v\in\eta_{\mathcal{I}}(A)$ ( $v\in\eta_{\mathcal{I}}(r))$ consumes time $O({\mathsf{d}}\cdot{|\Delta^{\mathcal{I}}|})$ ( $O({\mathsf{d}}\cdot{{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ ).

Assumption (1) is standard when analysing worst-case complexity. The others are pessimistic assumptions on the implementation of $\eta_{\mathcal{I}}$ (and $\eta_{\mathcal{I}}^{*}$ ). E.g., encoding the binary vectors as integers and implementing bit wise operations could reduce the complexity of membership access and iteration. Also, using a hash map with a perfect hash function would decrease the membership check to constant time.

We are now ready to present our upper bounds. For normalised ${\cal ELH}$ CIs, we provide Algorithm 1 to decide if a concept inclusion holds in a convex geometric model built as in Definition 29. Theorem 31 guarantees that $\eta_{\mathcal{I}}^{*}\models C\sqsubseteq D$ iff $\eta_{\mathcal{I}}\models C\sqsubseteq D$ for any CI in normalised ${\cal ELH}$ . Thus, as long as $\Delta^{\mathcal{I}}$ is finite, Algorithm 1 terminates and outputs whether $\eta_{\mathcal{I}}^{*}\models C\sqsubseteq D$ . Theorem 35 establishes that Algorithm 1 runs in polynomial time in the size of $\Delta^{\mathcal{I}}$ and the dimension of vectors in $\eta_{\mathcal{I}}^{*}$ .

Algorithm 1 Check if a convex geometric model (Definition 29) satisfies an

{\cal ELH}

CI in normal form.

Theorem 35.

Given a finite geometric interpretation $\eta_{\mathcal{I}}$ and an ${\cal ELH}$ CI in normal form, Algorithm 1 runs in time in $O({\mathsf{d}}\cdot{\mathsf{n}}^{4})$ , where ${\mathsf{d}}$ is as in Definition 19 and ${\mathsf{n}}=|\Delta^{\mathcal{I}}|$ .

As ${\mathsf{d}}$ depends linearly on $\Delta^{\mathcal{I}}$ and the size of the signature. If the latter is regarded as a constant, we can simply say that Algorithm 1 has time in $O({\mathsf{n}}^{5})$ , where ${\mathsf{n}}={|\Delta^{\mathcal{I}}|}$ . Similarly as for Algorithm 1, Theorem 31 allows us to design an algorithm to determine if a convex geometric model $\eta_{\mathcal{I}}^{*}$ satisfies an IQ in normal form $\alpha$ , as we show in Algorithm 2.

Algorithm 2 check if a convex geometric model (as in Definition 29) satisfies an

{\cal ELH}

IQ in normal form.

Theorem 36 shows that Algorithm 2 runs in time polynomial in ${\mathsf{d}}\cdot{|\Delta^{\mathcal{I}}|}$ .

Theorem 36.

Given a finite geometric interpretation $\eta_{\mathcal{I}}$ and an ${\cal ELH}$ IQ in normal form, Algorithm 2 runs in time $O({\mathsf{d}}\cdot{\mathsf{n}}^{3})$ , with ${\mathsf{d}}$ as in Definition 19 and ${\mathsf{n}}=|\Delta^{\mathcal{I}}|$ .

Next, we present Algorithm 3, which handles RIs. Again, as a consequence of Theorem 31, we only need to check the inclusion between two finite sets of vectors in $\mathbb{R}^{2\cdot{\mathsf{d}}}$ . Finally, we show an upper bound using Algorithm 3.

Algorithm 3 Check if a convex geometric model (as in Definition 29) satisfies an

{\cal ELH}

role inclusion.

Theorem 37.

Given a finite geometric interpretation $\eta_{\mathcal{I}}$ and an ${\cal ELH}$ role inclusion, Algorithm 3 runs in time in $O({\mathsf{d}}\cdot{\mathsf{n}}^{4})$ , where ${\mathsf{d}}$ is as in Definition 19 and ${\mathsf{n}}=|\Delta^{\mathcal{I}}|$ .

The three algorithms presented in this Section run in polynomial time in ${\mathsf{d}}\cdot{|\Delta^{\mathcal{I}}|}$ . We recall that the construction of $\eta_{\mathcal{I}}$ (and also $\eta_{\mathcal{I}}^{*}$ ) requires that both the signature and $\Delta^{\mathcal{I}}$ are finite (which is reasonable for normalized ${\cal ELH}$ ), otherwise the vectors in $\eta_{\mathcal{I}}$ would have infinite dimension.

7 Conclusion and discussion

We have proven that ${\cal ELH}$ has the strong faithfulness property over (possibly) non-convex geometric models, and that normalized ${\cal ELH}$ has the strong faithfulness property over convex geometric models. Furthermore, we give upper bounds for the complexity of checking satisfaction for ${\cal ELH}$ axioms in normal form in the class of convex geometric models that we use for strong faithfulness.

As future work, we would like to implement an embedding method that is formally guaranteed to generate strongly TBox faithful embeddings for normalized ${\cal ELH}$ ontologies, as well as expand the language so as to cover more logical constructs present in $\mathcal{EL}^{++}$ .

References

[1] Ralph Abboud, Ismail Ceylan, Thomas Lukasiewicz, and Tommaso Salvatori. BoxE: A box embedding model for knowledge base completion. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 9649–9661. Curran Associates, Inc., 2020. doi:10.5555/3495724.3496533.
[2] Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler. An Introduction to Description Logic. Cambridge University Press, USA, 1st edition, 2017. doi:10.1017/9781139025355.
[3] Antoine Bordes, Nicolas Usunier, Alberto Garcia-Duran, Jason Weston, and Oksana Yakhnenko. Translating embeddings for modeling multi-relational data. In C. J. Burges, L. Bottou, M. Welling, Z. Ghahramani, and K. Q. Weinberger, editors, Advances in Neural Information Processing Systems, volume 26. Curran Associates, Inc., 2013. doi:10.5555/2999792.2999923.
[4] Stefan Borgwardt and Veronika Thost. LTL over EL Axioms. Technische Universität Dresden, 2015. doi:10.25368/2022.213.
[5] Camille Bourgaux, Ricardo Guimarães, Raoul Koudijs, Victor Lacerda, and Ana Ozaki. Knowledge base embeddings: Semantics and theoretical properties. In Proceedings of the TwentyFirst International Conference on Principles of Knowledge Representation and Reasoning, pages 823–833, Hanoi, Vietnam, November 2024. International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/kr.2024/77.
[6] Camille Bourgaux, Ana Ozaki, and Jeff Z. Pan. Geometric models for (temporally) attributed description logics. In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, DL, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021. URL: https://ceur-ws.org/Vol-2954/paper-7.pdf.
[7] Jiaoyan Chen, Pan Hu, Ernesto Jimenez-Ruiz, Ole Magnus Holter, Denvar Antonyrajah, and Ian Horrocks. Owl2vec*: embedding of owl ontologies. Machine Learning, 110(7):1813–1845, July 2021. doi:10.1007/s10994-021-05997-6.
[8] Yuanfei Dai, Shiping Wang, Neal N. Xiong, and Wenzhong Guo. A Survey on Knowledge Graph Embedding: Approaches, Applications and Benchmarks. Electronics, 9(5):750, May 2020. doi:10.3390/electronics9050750.
[9] Claudia d’Amato, Nicola Flavio Quatraro, and Nicola Fanizzi. Injecting background knowledge into embedding models for predictive tasks on knowledge graphs. In Ruben Verborgh, Katja Hose, Heiko Paulheim, Pierre-Antoine Champin, Maria Maleshkova, Oscar Corcho, Petar Ristoski, and Mehwish Alam, editors, The Semantic Web, pages 441–457. Springer International Publishing, 2021. doi:10.1007/978-3-030-77385-4_26.
[10] Víctor Gutiérrez-Basulto and Steven Schockaert. From knowledge graph embedding to ontology embedding? an analysis of the compatibility between vector space representations and rules. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, KR, pages 379–388. AAAI Press, 2018. URL: https://aaai.org/ocs/index.php/KR/KR18/paper/view/18013, doi:10.4230/OASIcs.AIB.2022.3.
[11] Peter Gärdenfors. Conceptual Spaces: The Geometry of Thought. The MIT Press, March 2000. doi:10.7551/mitpress/2076.001.0001.
[12] Pascal Hitzler, Markus Krötzsch, and Sebastian Rudolph. Foundations of Semantic Web Technologies. Chapman & Hall/CRC, 2009.
[13] Anders Imenes, Ricardo Guimarães, and Ana Ozaki. Marrying query rewriting and knowledge graph embeddings. In RuleML+RR, pages 126–140. Springer-Verlag, 2023. doi:10.1007/978-3-031-45072-3_9.
[14] Mathias Jackermeier, Jiaoyan Chen, and Ian Horrocks. Dual box embeddings for the description logic el ${}^{\mbox{++}}$ . In Tat-Seng Chua, Chong-Wah Ngo, Ravi Kumar, Hady W. Lauw, and Roy Ka-Wei Lee, editors, Proceedings of the ACM on Web Conference, WWW, pages 2250–2258. ACM, 2024. doi:10.1145/3589334.3645648.
[15] Maxat Kulmanov, Wang Liu-Wei, Yuan Yan, and Robert Hoehndorf. EL embeddings: Geometric construction of models for the description logic EL++. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 6103–6109. ijcai.org, 2019. doi:10.24963/ijcai.2019/845.
[16] Victor Lacerda, Ana Ozaki, and Ricardo Guimarães. Faithel: Strongly tbox faithful knowledge base embeddings for $\mathcal{EL}$ . In Sabrina Kirrane, Mantas Šimkus, Ahmet Soylu, and Dumitru Roman, editors, Rules and Reasoning, pages 191–199, Cham, 2024. Springer Nature Switzerland. doi:10.1007/978-3-031-72407-7_14.
[17] Yankai Lin, Zhiyuan Liu, Maosong Sun, Yang Liu, and Xuan Zhu. Learning entity and relation embeddings for knowledge graph completion. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1), February 2015. doi:10.1609/aaai.v29i1.9491.
[18] Carsten Lutz and Frank Wolter. Deciding inseparability and conservative extensions in the description logic el. Journal of Symbolic Computation, 45(2):194–228, February 2010. doi:10.1016/j.jsc.2008.10.007.
[19] Sutapa Mondal, Sumit Bhatia, and Raghava Mutharaju. Emel++: Embeddings for EL++ description logic. In Andreas Martin, Knut Hinkelmann, Hans-Georg Fill, Aurona Gerber, Doug Lenat, Reinhard Stolle, and Frank van Harmelen, editors, AAAI-MAKE, volume 2846 of CEUR Workshop Proceedings. CEUR-WS.org, 2021. URL: https://ceur-ws.org/Vol-2846/paper19.pdf.
[20] Özgür Lütfü Özçep, Mena Leemhuis, and Diedrich Wolter. Cone semantics for logics with negation. In Christian Bessiere, editor, IJCAI, pages 1820–1826. ijcai.org, 2020. doi:10.24963/ijcai.2020/252.
[21] Aleksandar Pavlovic and Emanuel Sallinger. ExpressivE: A spatio-functional embedding for knowledge graph completion. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL: https://openreview.net/pdf?id=xkev3_np08z.
[22] Xi Peng, Zhenwei Tang, Maxat Kulmanov, Kexin Niu, and Robert Hoehndorf. Description logic EL++ embeddings with intersectional closure. CoRR, abs/2202.14018, 2022. arXiv:2202.14018, doi:10.48550/arXiv.2202.14018.
[23] Xi Peng, Zhenwei Tang, Maxat Kulmanov, Kexin Niu, and Robert Hoehndorf. Description logic EL++ embeddings with intersectional closure. CoRR, abs/2202.14018, 2022. arXiv:2202.14018.
[24] Théo Trouillon, Johannes Welbl, Sebastian Riedel, Éric Gaussier, and Guillaume Bouchard. Complex embeddings for simple link prediction. arXiv, June 2016. doi:10.48550/arXiv.1606.06357.
[25] Denny Vrandečić and Markus Krötzsch. Wikidata: A free collaborative knowledgebase. Commun. ACM, 57(10):78–85, September 2014. doi:10.1145/2629489.
[26] Bo Xiong, Nico Potyka, Trung-Kien Tran, Mojtaba Nayyeri, and Steffen Staab. Faithful embeddings for EL++ knowledge bases. In The Semantic Web – ISWC 2022, pages 22–38. Springer International Publishing, 2022. doi:10.1007/978-3-031-19433-7_2.
[27] Bishan Yang, Wen-tau Yih, Xiaodong He, Jianfeng Gao, and Li Deng. Embedding entities and relations for learning and inference in knowledge bases. arXiv, August 2015. arXiv:1412.6575.
[28] Frank Zenker and Peter Gärdenfors. Applications of Conceptual Spaces: The Case for Geometric Knowledge Representation, volume 359 of Synthese Library. Springer International Publishing, 2015. doi:10.1007/978-3-319-15021-5.

Appendix A Appendix

A.1 Omitted proofs for Section 3

See 5

Proof.

Let $S_{1},S_{2}$ be finite sets with $S_{1}\subseteq S_{2}$ . We first prove the statement for $v\in S_{1}\subseteq S^{\ast}_{1}$ and then for $u\in S_{1}^{\ast}\setminus S_{1}$ . Let $v\in S_{1}$ be an arbitrary vector. By assumption, $v\in S_{2}$ , and by the definition of convex hull, $v\in S_{2}^{\ast}$ . Now, by Definition 4 let $u\in S_{1}^{\ast}\setminus S_{1}$ be defined by $\sum_{i=1}^{n}\lambda_{i}v_{i}$ where $v_{1}\ldots v_{n}\in S_{1}$ and $n\leq|S_{1}|$ . Since $S_{1}\subseteq S_{2}$ , $v_{1}\ldots v_{n}\in S_{2}$ and, by Definition 4, since $u=\sum_{i=1}^{n}\lambda_{i}v_{i}$ , this gives us that $u\in S_{2}^{\ast}$ . Thus, $S_{1}\subseteq S_{2}$ implies $S_{1}^{\ast}\subseteq S_{2}^{\ast}$ . $\hfill\blacktriangleleft$

See 6

Proof.

For this proof we use a notation introduced in Definition 19. We reason by cases. We need to cover all combinations of values that $\lambda_{i}$ may take for arbitrary $n$ . We cover two cases. One where all $\lambda$ are strictly greater than zero and strictly lesser than 1, and a case where some $\lambda_{i}$ may be zero. By setting $n=1$ , we have $v=\lambda_{1}x_{1}$ . By definition, $\lambda_{1}=1$ , giving us either $v=0$ or $v=1$ , both binary vectors, which means $v\in S^{*}$ iff $v\in S$ . Therefore, this case is not in the scope of our lemma, and we assume $n>1$ .

$\blacksquare$

Case 1 ( $0<\lambda_{i}<1$ ): We prove the case by induction on the number of $n$ .
Base case: In the base case $n=2$ . Let $v_{1},v_{2}\in S$ with $v_{1}\neq v_{2}$ . Then, there is a dimension $d$ such that $v_{1}[d]\neq v_{2}[d]$ . Since $v_{1}$ and $v_{2}$ are binary, we can assume, without loss of generality, $v_{1}[d]=1$ and $v_{2}[d]=0$ . Now let $v=\lambda_{1}v_{1}+\lambda_{2}v_{2}$ be a vector, with $\lambda_{1}+\lambda_{2}=1$ . Since we assumed $\forall\lambda_{i}$ $0<\lambda_{i}<1$ , this means $v\not\in\{0,1\}^{d}$ because $v[d]=\lambda_{1}$ , which is strictly between 0 and 1. Therefore, $v$ is non-binary.
Inductive step: Assume our hypothesis holds for $v_{1},\ldots,v_{n-1}$ .

Let $v\in S^{*}$ . We know that $v=\sum_{i=1}^{n}\lambda_{i}v_{i}$ , with $0<\lambda_{i}<1$ , with $v_{i}\in S$ , and with $\sum_{i=1}^{n}\lambda_{i}=1$ . Since $\forall_{i\neq j}\,v_{i}\neq v_{j}$ , there is a dimension $d$ such that $\exists l,m$ with $v_{l}[d]\neq v_{m}[d]$ . Since $S$ is a set of binary vectors, we decompose the value of a dimension $d$ as a sum of vectors where $v_{i}[d]=1$ and $v_{j}[d]=0$ . In order to do this, we introduce an ordering and assume, without loss of generality, that $v_{i}[d]=1$ $\forall 1\leq i\leq k$ where $k<n$ , and $v_{j}[d]=0$ $\forall k+1\leq j<n$ . More explicitly:

$v[d]=\sum_{i=1}^{k}\lambda_{i}v_{i}[d]+\sum_{j=k+1}^{n}\lambda_{j}v_{j}[d].$

However, $\sum_{j=k+1}^{n}\lambda_{j}v_{j}[d]=0$ , so we only have to look at the first sum. Clearly, $v[d]\neq 0$ , because $v_{l}[d]\neq v_{m}[d]$ . Since there exists at least one $\lambda_{j}>0$ and, in this case $\forall\lambda_{i}$ $0<\lambda_{i}<1$ , it is impossible for the sum to be equal to $1$ , giving us $v[d]\in(0,1)$ .
$\blacksquare$

Case 2 ( $\exists\lambda_{i}=0$ and $\forall\lambda_{j\neq i}$ we have $0\leq\lambda_{j}<1$ ):

We prove the case directly. We start by noting that for this case to hold, $n\geq 3$ , as $n=2$ would mean $\lambda_{1}=0$ and $\lambda_{2}<1$ , which goes against the criterion that $\sum_{i=1}^{n}\lambda_{i}v_{i}=1$ from the definition. Now, assume $n\geq 3$ . We denote by $m$ the number of $\lambda_{i}$ where $\lambda_{i}=0$ . Pick $m$ such that $1\leq m\leq n-2$ . Then, there are at least $n-m\geq 2$ $\lambda_{j}$ such that $0<\lambda_{j}<1$ . Which is the situation covered by Case 1.

There are no more cases to be considered. $\hfill\blacktriangleleft$

See 7

Proof.

The corollary follows directly from Theorem 6. $\hfill\blacktriangleleft$

A.2 Omitted proofs for Section 4

Lemma 38.

For all $d\in\Delta^{\mathcal{I}}$ , for all ${\cal ELH}$ concepts $C$ , it is the case that $d\in C^{\mathcal{I}}$ iff $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C)$ (see Definition 12).

Proof.

We provide an inductive argument in order to prove the claim.

Base case:

Assume $C=A\in N_{C}$ , and assume $d\in A^{\mathcal{I}}$ .

By the definition of $\bar{\eta}_{\mathcal{I}}$ , $d\in A^{\mathcal{I}}$ iff for all $v\in\bar{\mu}(d)$ , $v\in\bar{\eta}_{\mathcal{I}}(A)$ , that is, iff $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(A)$ . Now assume $C=\top$ , and assume $d\in C^{\mathcal{I}}$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , if $d\in C^{\mathcal{I}}$ , then $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C)$ . Now assume $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C)$ . Since we assumed $C=\top$ , we have that $\bar{\mu}(d)\subseteq\mathbb{R}^{1}$ , with $d\in\Delta^{\mathcal{I}}$ . When $C=\bot$ , the statement is vacuously true.

Inductive step:

Assume our hypothesis holds for $C_{1}$ and $C_{2}$ . There are two cases:

$\blacksquare$

Case 1 $(C_{1}\sqcap C_{2})$ : Assume $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ by the semantics of ${\cal ELH}$ , $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ iff $d\in C_{1}^{\mathcal{I}}$ and $d\in C_{2}^{\mathcal{I}}$ . By the inductive hypothesis, $d\in C_{i}^{\mathcal{I}}$ iff $\bar{\mu}(d)\subseteq\eta_{\mathcal{I}}(C_{i})$ , $i\in\{1,2\}$ . But this happens iff $d\in\bar{\eta}_{\mathcal{I}}(C_{1})\cap\bar{\eta}_{\mathcal{I}}(C_{2})$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , this means that $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C_{1}\sqcap C_{2})$ iff $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ .
$\blacksquare$

Case 2 $(\exists r.C_{1})$ : Assume $d\in(\exists r.C_{1})^{\mathcal{I}}$ by the semantics of ${\cal ELH}$ , $d\in(\exists r.C_{1})^{\mathcal{I}}$ iff $(d,e)\in r^{\mathcal{I}}$ and $e\in C_{1}^{\mathcal{I}}$ . By the inductive hypothesis, $e\in C_{1}^{\mathcal{I}}$ iff $\bar{\mu}(e)\subseteq\bar{\eta}_{\mathcal{I}}(C_{1})$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , $(d,e)\in r^{\mathcal{I}}$ iff $f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ where $v\in\bar{\mu}(d)$ . By the semantics of $\bar{\eta}_{\mathcal{I}}$ , $f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ and $e\in\bar{\eta}_{\mathcal{I}}(C_{1})$ iff $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(\exists r.C_{1})$ .

$\hfill\blacktriangleleft$

Lemma 39.

For all interpretations $\mathcal{I}$ , all ${\cal ELH}$ concepts $C$ , and all $a\in N_{I}$ , it is the case that $\mathcal{I}$ $\models C(a)$ iff $\bar{\eta}_{\mathcal{I}}\models C(a)$

Proof.

By the semantics of ${\cal ELH}$ , we know $\mathcal{I}\models C(a)$ iff $a^{\mathcal{I}}\in C^{\mathcal{I}}$ . By Lemma 38, we know that $a^{\mathcal{I}}\in C^{\mathcal{I}}$ iff $\bar{\eta}_{\mathcal{I}}(a^{\mathcal{I}})\in\bar{\eta}_{\mathcal{I}}(C)$ . By the semantics of geometric interpretation, this is the case iff $\bar{\eta}_{\mathcal{I}}\models C(a)$ . $\hfill\blacktriangleleft$

Lemma 40.

For all $r\in N_{R}$ , for all $a,b\in N_{I}$ , we have $\bar{\eta}_{\mathcal{I}}\models r(a,b)$ iff $\mathcal{I}\models r(a,b)$ .

Proof.

By the semantics of ${\cal ELH}$ , $\mathcal{I}\models r(a,b)$ iff $(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , we have $(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$ iff $f(v,b^{\mathcal{I}})\in\bar{\eta}_{\mathcal{I}}(r)$ for all $v\in\bar{\mu}(a^{\mathcal{I}})$ . From the Definition 12, $b^{\mathcal{I}}=\bar{\eta}_{\mathcal{I}}(b)$ , hence $(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$ iff $f(v,\bar{\eta}_{\mathcal{I}}(b))\in\bar{\eta}_{\mathcal{I}}(r)$ for all $v\in\bar{\mu}(a^{\mathcal{I}})$ . Since $\bar{\eta}_{\mathcal{I}}(a)\in\bar{\mu}(a^{\mathcal{I}})$ , we get, by the semantics of $\bar{\eta}_{\mathcal{I}}$ , that $f(\bar{\eta}_{\mathcal{I}}(a),\bar{\eta}_{\mathcal{I}}(b))\in\bar{\eta}_{% \mathcal{I}}(r)$ iff $\bar{\eta}_{\mathcal{I}}\models r(a,b)$ . Giving us $\mathcal{I}\models r(a,b)$ iff $\bar{\eta}_{\mathcal{I}}\models r(a,b)$ . $\hfill\blacktriangleleft$

Lemma 41.

Let $\mathcal{O}$ be an ${\cal ELH}$ ontology and let ${\bar{\mathcal{I}}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (Definition 14). The geometrical interpretation $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}$ of ${\bar{\mathcal{I}}_{\mathcal{O}}}$ (Definition 12) is a strongly IQ faithful model of $\mathcal{O}$ .

Proof.

Since $\mathcal{I}_{\mathcal{O}}$ is a canonical model of $\mathcal{O}$ , $\mathcal{I}_{\mathcal{O}}\models\alpha$ iff $\mathcal{O}\models\alpha$ (Theorem 15). By Lemmas 39 and 40, $\mathcal{I}_{\mathcal{O}}\models\alpha$ iff $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}\models\alpha$ . Then, we have that $\mathcal{O}\models\alpha$ iff $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}\models\alpha$ . $\hfill\blacktriangleleft$

Lemma 42.

Let $\mathcal{I}$ be an interpretation, and $\bar{\mu}$ be a mapping derived from Definition 10. For all ${\cal ELH}$ concepts $C$ , if $v\in\bar{\eta}_{\mathcal{I}}(C)$ , then there is $d\in\Delta^{\mathcal{I}}$ such that $v\in\bar{\mu}(d)$ , and $d\in C^{\mathcal{I}}$ .

Proof.

We provide an inductive argument for the claim.

Base case:

Assume $C=A\in N_{C}$ and let $v\in\bar{\eta}_{\mathcal{I}}(A)$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , it is the case that $v\in\bar{\eta}_{\mathcal{I}}(A)$ iff $v\in\{v^{\prime}\in\bar{\mu}(d)\mid d\in A^{\mathcal{I}}\}$ . Assume $C=\top$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , we have $v\in\bar{\eta}_{\mathcal{I}}(C)$ iff $v\in\bar{\mu}(d)$ such that $\bar{\mu}(d)\subseteq\mathbb{R}^{1}$ . This means $v\in\bar{\mu}(d)$ and $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C)$ , for some $d\in\Delta^{\mathcal{I}}$ . When $C=\bot$ , the statement is vacuously true.

Inductive step:

Assume our hypothesis holds for $C_{1}$ and $C_{2}$ .

$\blacksquare$

Case 1 ( $C_{1}\sqcap C_{2})$ : Assume $v\in\bar{\eta}_{\mathcal{I}}(C_{1}\sqcap C_{2})$ . Then, by the definition of $\bar{\eta}_{\mathcal{I}}$ , it is the case that $v\in\bar{\eta}_{\mathcal{I}}(C_{1})$ and $v\in\bar{\eta}_{\mathcal{I}}(C_{2})$ . By the inductive hypothesis, if $v\in\bar{\eta}_{\mathcal{I}}(C_{1})$ , then $\exists d\in\Delta^{\mathcal{I}}$ such that $v\in\bar{\mu}(d)$ and $d\in C^{\mathcal{I}}_{1}$ , and if $v\in\bar{\eta}_{\mathcal{I}}(C_{2})$ , then $\exists d^{\prime}\in\Delta^{\mathcal{I}}$ such that $v\in\bar{\mu}(d^{\prime})$ and $d^{\prime}\in C^{\mathcal{I}}_{2}$ . By definition of $\bar{\mu}$ , this can only be if $d^{\prime}=d$ since $\bar{\mu}$ maps elements of $\Delta^{\mathcal{I}}$ to mutually disjoint subsets of $\mathbb{R}^{1}$ . By the semantics of ${\cal ELH}$ , if $d\in C^{\mathcal{I}}_{1}$ and $d\in C^{\mathcal{I}}_{2}$ then $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ .
$\blacksquare$

Case 2 $(\exists r.C_{1})$ : Assume $v\in\bar{\eta}_{\mathcal{I}}(\exists r.C_{1})$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , this means $v$ is such that $f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ where $v\in\bar{\mu}(d)$ for $(d,e)\in r^{\mathcal{I}}$ and $e\in\bar{\eta}_{\mathcal{I}}(C_{1})$ . By the inductive hypothesis, there is an $e^{\prime}\in\Delta^{\mathcal{I}}$ such that $e\in\bar{\mu}(e^{\prime})$ and $e^{\prime}\in C_{1}^{\mathcal{I}}$ . As $e^{\prime}\in\Delta^{\mathcal{I}}\subseteq\mathbb{N}$ , by the construction of $\bar{\mu}$ , it is the case that $e^{\prime}=e$ . Therefore, we have $e\in C_{1}^{\mathcal{I}}$ . By the definition of $\bar{\mu}$ and the semantics of ${\cal ELH}$ , this means $\exists d\in\Delta^{\mathcal{I}}$ such that $v\in\bar{\mu}(d)$ and $d\in(\exists r.C_{1})^{\mathcal{I}}$ .

$\hfill\blacktriangleleft$

Lemma 43.

Let $\mathcal{I}$ be an interpretation and $\bar{\eta}_{\mathcal{I}}$ the geometric interpretation of $\mathcal{I}$ (Definition 12). For all ${\cal ELH}$ concepts $C$ and $D$ , $\mathcal{I}\models C\sqsubseteq D$ iff $\bar{\eta}_{\mathcal{I}}\models C\sqsubseteq D$ .

Proof.

Let $C, D$ be ${\cal ELH}$ concepts. Assume $\mathcal{I}\models C\sqsubseteq D$ . By the semantics of ${\cal ELH}$ , this means $C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$ . Let $v\in\bar{\eta}_{\mathcal{I}}(C)$ be a vector. By Lemma 42, we know there is $d\in\Delta^{\mathcal{I}}$ and $d\in C^{\mathcal{I}}$ such that $v\in\bar{\mu}(d)$ and $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C)$ . By Lemma 38, this means $d\in C^{\mathcal{I}}$ , and, by assumption, that $d\in D^{\mathcal{I}}$ . By Lemma 38, this means $\bar{\mu}(d)\subseteq\eta_{\mathcal{I}}(D)$ . Since we have shown $v\in\bar{\mu}(d)$ such that $\bar{\eta}_{\mathcal{I}}(C)$ implies $v\in\bar{\eta}_{\mathcal{I}}(D)$ , this means $\bar{\eta}_{\mathcal{I}}\models C\sqsubseteq D$ .

Now assume $\bar{\eta}_{\mathcal{I}}\models C\sqsubseteq D$ . By the semantics of geometric interpretation, this means $\bar{\eta}_{\mathcal{I}}(C)\subseteq\bar{\eta}_{\mathcal{I}}(D)$ . Let $d\in C^{\mathcal{I}}$ . We know, by Lemma 38, that $d\in C^{\mathcal{I}}$ iff $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(C)$ . By assumption, this means $\bar{\mu}(d)\subseteq\bar{\eta}_{\mathcal{I}}(D)$ . Again by Lemma 38, this means $d\in D^{\mathcal{I}}$ . Since we have shown $d\in C^{\mathcal{I}}$ implies $d\in D^{\mathcal{I}}$ , we have $\mathcal{I}\models C\sqsubseteq D$ . $\hfill\blacktriangleleft$

Lemma 44.

Let $\mathcal{I}$ be an interpretation, $\bar{\mu}$ be a mapping (Definition 10), and $\bar{\eta}_{\mathcal{I}}$ the geometric interpretation of $\mathcal{I}$ (Definition 12) derived from $\bar{\mu}$ . For all role names $r\in N_{R}$ , if $f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ , then there are $d,e\in\Delta^{\mathcal{I}}$ such that $v\in\bar{\mu}(d)$ for $(d,e)\in r^{\mathcal{I}}$ .

Proof.

Assume $z=f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ . By the definition of $\bar{\eta}_{\mathcal{I}}$ , we have $z\in\{f(v,e)\mid v\in\bar{\mu}(d)\text{ for }(d,e)\in r^{\mathcal{I}}$ }. This means $v\in\bar{\mu}(d)$ for $d\in\Delta^{\mathcal{I}}$ , and, by definition, $e\in\Delta^{\mathcal{I}}$ . $\hfill\blacktriangleleft$

Lemma 45.

Let $\mathcal{I}$ be an interpretation and $\bar{\eta}_{\mathcal{I}}$ the geometric interpretation of $\mathcal{I}$ (Definition 12). For all roles $r,s\in N_{R}$ , it is the case that $\mathcal{I}\models r\sqsubseteq s$ iff $\bar{\eta}_{\mathcal{I}}\models r\sqsubseteq s$ .

Proof.

Assume $\mathcal{I}\models r\sqsubseteq s$ . By the semantics of ${\cal ELH}$ , $r^{\mathcal{I}}\subseteq s^{\mathcal{I}}$ . Now let $v\in\bar{\eta}_{\mathcal{I}}(r)$ . By Lemma 44, there is $d\in\Delta^{\mathcal{I}}$ such that $v\in\bar{\mu}(d)$ , $e\in\Delta^{\mathcal{I}}$ , and $(d,e)\in r^{\mathcal{I}}$ . By assumption, this gives us $(d,e)\in s^{\mathcal{I}}$ . By the construction of $\bar{\eta}_{\mathcal{I}}$ , this means $f(v,e)\in\bar{\eta}_{\mathcal{I}}(s)$ for $v\in\bar{\mu}(d)$ . Hence, $f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ implies $f(v,e)\in\bar{\eta}_{\mathcal{I}}(s)$ and we can conclude that $\bar{\eta}_{\mathcal{I}}\models r\sqsubseteq s$ . Now assume $\bar{\eta}_{\mathcal{I}}\models r\sqsubseteq s$ . By the semantics of $\bar{\eta}_{\mathcal{I}}$ , $\bar{\eta}_{\mathcal{I}}(r)\subseteq\bar{\eta}_{\mathcal{I}}(s)$ . Let $(d,e)\in r^{\mathcal{I}}$ . From the definition of $\bar{\eta}_{\mathcal{I}}$ , we know there is $f(v,e)\in\bar{\eta}_{\mathcal{I}}(r)$ such that $v\in\bar{\mu}(d)$ . By assumption, we have $f(v,e)\in\bar{\eta}_{\mathcal{I}}(s)$ and, by the definition of $\bar{\eta}_{\mathcal{I}}$ , this is the case iff $(d,e)\in s^{\mathcal{I}}$ . Since $(d,e)$ was arbitrary, we conclude $\mathcal{I}\models r\sqsubseteq s$ . $\hfill\blacktriangleleft$

See 13

Proof.

For the case where $\alpha$ is a concept inclusion, the result comes from Lemma 43. For the case where $\alpha$ is a role inclusion, the result comes from Lemma 45. For the case where $\alpha$ is an IQ, the result comes from Lemma 39 and from Lemma 40. $\hfill\blacktriangleleft$

Lemma 46.

Let $\mathcal{O}$ be an ${\cal ELH}$ ontology and let ${\bar{\mathcal{I}}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (see Definition 14). The $m$ -dimensional $f$ -geometric interpretation of ${\bar{\mathcal{I}}_{\mathcal{O}}}$ (see Definition 12) is a strongly TBox faithful model of $\mathcal{O}$ . That is, $\mathcal{O}\models\tau$ iff $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}\models\tau$ , where $\tau$ is either an $\mathcal{ELH_{\bot}}$ concept inclusion or an ${\cal ELH}$ role inclusion.

Proof.

Since we know ${\bar{\mathcal{I}}_{\mathcal{O}}}$ is canonical, $\mathcal{O}\models\alpha$ iff ${\bar{\mathcal{I}}_{\mathcal{O}}}\models\alpha$ . By Lemma 43 we know $\mathcal{I}\models C\sqsubseteq D$ iff $\bar{\eta}_{\mathcal{I}}\models C\sqsubseteq D$ , and by Lemma 45 we know $\mathcal{I}\models r\sqsubseteq s$ iff $\bar{\eta}_{\mathcal{I}}\models r\sqsubseteq s$ . This means that ${\bar{\mathcal{I}}_{\mathcal{O}}}\models C\sqsubseteq D$ iff $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}\models C\sqsubseteq D$ and ${\bar{\mathcal{I}}_{\mathcal{O}}}\models r\sqsubseteq s$ iff $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}\models r\sqsubseteq s$ , giving us $\mathcal{O}\models\tau$ iff $\bar{\eta}_{{\bar{\mathcal{I}}_{\mathcal{O}}}}\models\tau$ . $\hfill\blacktriangleleft$

See 16

Proof.

The theorem follows by Lemma 41 and by Lemma 46. $\hfill\blacktriangleleft$

A.3 Omitted proofs for Section 5

See 24

Proof.

We provide an inductive argument for the claim.

Base case:

Notice that if $\mu(d)=\mu(e)$ , then $\mu(d)[i]=n$ iff $\mu(e)[i]=n$ , for all $i$ . That is, the value at the $i t h$ index is $n$ for $\mu(d)$ and $\mu(e)$ , otherwise they would not be the same vector. Now, assume $C=A\in N_{C}$ , and $d\in C^{\mathcal{I}}$ . By the definition of $\mu$ , $\mu(d)[C]=1$ . Since $\mu(d)=\mu(e)$ , we have that $\mu(d)[C]=1$ iff $\mu(e)[C]=1$ . But, by the definition of $\mu$ , $\mu(e)[C]=1$ iff $e\in C^{\mathcal{I}}$ , thus giving us our result.

Inductive step:

Assume our hypothesis holds for $C_{1}$ and $C_{2}$ .

Assume $\mu(d)=\mu(e)$ . By the semantics of ${\cal ELH}$ , $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ iff $d\in C^{\mathcal{I}}_{1}$ and $d\in C^{\mathcal{I}}_{2}$ . By the induction hypothesis, this happens iff $e\in C^{\mathcal{I}}_{1}$ and $e\in C^{\mathcal{I}}_{2}$ . This means, of course, by the semantics of ${\cal ELH}$ , that $e\in C^{\mathcal{I}}_{1}$ and $e\in C^{\mathcal{I}}_{2}$ iff $e\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ . Finally, we get $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ iff $e\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ .

We prove the case $(\exists r.C_{1})$ directly. Assume $\mu(d)=\mu(e)$ , and $d\in(\exists r.C_{1})^{\mathcal{I}}$ . Then, by the semantics of ${\cal ELH}$ , $\exists d^{\prime}$ such that $d^{\prime}\in C^{\mathcal{I}}_{1}$ , and $r(d,d^{\prime})^{\mathcal{I}}$ . By the definition of $\mu$ , we know $\mu(d)[r,d^{\prime}]=1$ . But from our initial observation, $\mu(d)[r,d^{\prime}]=1$ iff $\mu(e)[r,d^{\prime}]=1$ . By definition of $\mu$ , $\mu(e)[r,d^{\prime}]=1$ iff $(e,d^{\prime})\in r^{\mathcal{I}}$ . By the semantics of ${\cal ELH}$ , whenever $d^{\prime}\in C_{1}^{\mathcal{I}}$ and $(e,d^{\prime})\in r^{\mathcal{I}}$ we have that $e\in(\exists r.C_{1})^{\mathcal{I}}$ . $\hfill\blacktriangleleft$

Lemma 47.

Let $\mathcal{I}$ be an interpretation, and $\mu$ a mapping derived from Definition 19. For all normalized $\mathcal{ELH}$ concepts $C$ , if $v\in\eta_{\mathcal{I}}(C)$ , then there is $d\in\Delta^{\mathcal{I}}$ such that $v=\mu(d)$ and $d\in C^{\mathcal{I}}$ .

Proof.

We provide an inductive argument for the claim.

Base case:

Assume $C=A\in N_{C}$ and assume $v\in\eta_{\mathcal{I}}(C)$ . By the definition of $\eta_{\mathcal{I}}$ , it is the case that $v\in\eta_{\mathcal{I}}(C)$ iff $v[C]=1$ . This is the case iff $v=\mu(d)$ , for some $d\in\Delta^{\mathcal{I}}$ .

Inductive step:

Assume our hypothesis holds for $C_{1}$ and $C_{2}$ . We prove two cases.

$\blacksquare$

Case 1 ( $C_{1}\sqcap C_{2}$ ): Assume $v\in\eta_{\mathcal{I}}(C_{1}\sqcap C_{2})$ . Then, by definition of $\eta_{\mathcal{I}}$ , it is true that $v\in\eta_{\mathcal{I}}(C_{1})$ and $v\in\eta_{\mathcal{I}}(C_{2})$ . By the inductive hypothesis, if this is the case, then $v=\mu(d)\in C_{1}$ and $v=\mu(d)\in C_{2}$ , for $d\in\Delta^{\mathcal{I}}$ . This gives us $v=\mu(d)\in\eta_{\mathcal{I}}(C_{1})\cap\eta_{\mathcal{I}}(C_{2})$ , which means $v=\mu(d)\in\eta_{\mathcal{I}}(C_{1}\sqcap C_{2})$ , for $d\in\Delta^{\mathcal{I}}$ .
$\blacksquare$

Case 2 ( $\exists r.C_{1}$ ): Assume $v\in\eta_{\mathcal{I}}(\exists r.C_{1})$ . Then, by the definition of $\eta_{\mathcal{I}}$ , $\exists u\in\eta_{\mathcal{I}}(C_{1})$ and $v\oplus u\in\eta_{\mathcal{I}}(r)$ . By the inductive hypothesis, if $u\in\eta_{\mathcal{I}}(C_{1})$ , we get $u=\mu(e)\in\eta_{\mathcal{I}}(C_{1})$ , for $e\in\Delta^{\mathcal{I}}$ . Now, $v\oplus u\in\eta_{\mathcal{I}}(r)$ iff $v\oplus u\in\{\mu(d)\oplus\mu(e)\mid\mu(d)[r,e]=1\}$ , for $d,e\in\Delta^{\mathcal{I}}$ . This gives us $v=\mu(d)$ such that $\mu(d)[r,e]=1$ . By construction of $\eta_{\mathcal{I}}$ , if we have $u=\mu(e)\in\eta_{\mathcal{I}}(C_{1})$ , and $v=\mu(d)$ such that $\mu(d)[r,e]=1$ with $v\oplus u\in\eta_{\mathcal{I}}(r)$ , this means $v=\mu(d)\in\eta_{\mathcal{I}}(\exists r.C_{1})$ , for some $d\in\Delta^{\mathcal{I}}$ .

$\hfill\blacktriangleleft$

Lemma 48.

Let $\mathcal{I}$ be an interpretation and let $\mu$ be as in Definition 19. For all $r\in N_{R}$ , if $u\oplus w\in\eta_{\mathcal{I}}(r)$ , then there are $d,e\in\Delta^{\mathcal{I}}$ such that $u=\mu(d)$ , $w=\mu(e)$ , and $(d,e)\in r^{\mathcal{I}}$ .

Proof.

Assume $v=u\oplus w\in\eta_{\mathcal{I}}(r)$ . Then, by the definition of $\eta_{\mathcal{I}}(r)$ , it is the case that $v\in\{\mu(d)\oplus\mu(e)\mid\mu(d)[r,e]=1\text{, for }d,e\in\Delta^{\mathcal{I% }}\}$ . This means there are $d,e\in\Delta^{\mathcal{I}}$ such that $v=\mu(d)\oplus\mu(e)$ and $\mu(d)[r,e]=1$ . By construction of $\mu$ , it is true that $\mu(d)[r,e]=1$ iff $(d,e)\in r^{\mathcal{I}}$ . This means there are $d,e\in\Delta^{\mathcal{I}}$ such that $u=\mu(d)$ , $w=\mu(e)$ and $(d,e)\in r^{\mathcal{I}}$ . $\hfill\blacktriangleleft$

Lemma 49.

For all $d\in\Delta^{\mathcal{I}}$ , for all ${\cal ELH}$ concepts $C$ , $d\in C^{\mathcal{I}}$ iff $\mu(d)\in\eta_{\mathcal{I}}(C)$ .

Proof.

We provide an inductive argument for the claim.

For all $d\in\Delta^{\mathcal{I}}$ , for all ${\cal ELH}$ concepts $C$ , $d\in C^{\mathcal{I}}$ iff $\mu(d)\in\eta_{\mathcal{I}}(C)$ .

Base case:

Assume $C=A\in N_{C}$ and $d\in C^{\mathcal{I}}$ . By the definition of $\mu$ , $d\in C^{\mathcal{I}}$ iff $\mu(d)[C]=1$ . By the definition of geometric interpretation, $\mu(d)[C]=1$ iff $\mu(d)\in\eta_{\mathcal{I}}(C)$ .

Inductive step:

assume our hypothesis holds for $C_{1}$ and $C_{2}$ . We consider two cases:

$\blacksquare$

Case 1 $(C_{1}\sqcap C_{2})$ : Assume $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ . This is the case iff $d\in C_{1}^{\mathcal{I}}$ and $d\in C_{2}^{\mathcal{I}}$ . By the inductive hypothesis, we have that $\mu(d)\in\eta_{\mathcal{I}}(C_{1})$ and $d\in\eta_{\mathcal{I}}(C_{2})$ . But $\mu(d)\in\eta_{\mathcal{I}}(C_{1})$ and $d\in\eta_{\mathcal{I}}(C_{2})$ iff $\mu(d)\in\eta_{\mathcal{I}}(C_{1}\sqcap C_{2})$ . Finally, by the semantics of geometric interpretation, $\mu(d)\in\eta_{\mathcal{I}}(C_{1}\sqcap C_{2})$ iff $d\in(C_{1}\sqcap C_{2})^{\mathcal{I}}$ .
$\blacksquare$

Case 2 $(\exists r.C_{1})$ : Assume $d\in(\exists r.C_{1})^{\mathcal{I}}$ . Then, by the semantics of ${\cal ELH}$ , $\exists e\in C_{1}^{\mathcal{I}}$ such that $(d,e)\in r^{\mathcal{I}}$ . By the inductive hypothesis, we get $\mu(e)\in\eta_{\mathcal{I}}(C_{1})$ . By the definition of $\eta_{\mathcal{I}}$ , $(d,e)\in r^{\mathcal{I}}$ iff $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}(r)$ . But, by the semantics of our geometric interpretation, $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}(r)$ and $\mu(e)\in\eta_{\mathcal{I}}(C_{1})$ iff $\mu(d)\in\eta_{\mathcal{I}}(\exists r.C_{1})$ .

$\hfill\blacktriangleleft$

Lemma 50.

For all interpretations $\mathcal{I}$ , all ${\cal ELH}$ concepts $C$ , all $a\in N_{I}$ , $\mathcal{I}\models C(a)$ iff $\eta_{\mathcal{I}}\models C(a)$ .

Proof.

$\mathcal{I}\models C(a)$ iff $a^{\mathcal{I}}\in C^{\mathcal{I}}$ . By Lemma 49, $a^{\mathcal{I}}\in C^{\mathcal{I}}$ iff $\mu(a^{\mathcal{I}})\in\eta_{\mathcal{I}}(C)$ . By the semantics of geometric interpretation, $\mu(a^{\mathcal{I}})\in\eta_{\mathcal{I}}(C)$ iff $\eta_{\mathcal{I}}\models C(a)$ . $\hfill\blacktriangleleft$

Lemma 51.

For all $r\in N_{R}$ , all $a,b\in N_{I}$ , $\mathcal{I}\models r(a,b)$ iff $\eta_{\mathcal{I}}\models r(a,b)$ .

Proof.

Assume $\mathcal{I}\models r(a,b)$ . By the semantics of ${\cal ELH}$ , this means there are $d,e\in\Delta^{\mathcal{I}}$ such that $d=a^{\mathcal{I}}$ , $e=b^{\mathcal{I}}$ , and $(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$ . By the definition of $\mu$ , this means $\mu(d)[a]=1$ , that $\mu(e)[b]=1$ , and that $\mu(d)[r,e]=1$ . By the definition of geometric interpretation, this means $\mu(d)=\eta_{\mathcal{I}}(a)$ , that $\mu(e)=\eta_{\mathcal{I}}(b)$ , and that $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}(r)$ , which is the case iff $\eta_{\mathcal{I}}\models r(a,b)$ .

Now assume $\eta_{\mathcal{I}}\models r(a,b)$ . This means that $\eta_{\mathcal{I}}(a)\oplus\eta_{\mathcal{I}}(b)\in\eta_{\mathcal{I}}(r)$ . By Lemma 48, we have that $\exists d,e\in\Delta^{\mathcal{I}}$ such that $\eta_{\mathcal{I}}(a)=\mu(d)$ , $\eta_{\mathcal{I}}(b)=\mu(e)$ , and $(d,e)\in r^{\mathcal{I}}$ . But, by the definition of geometric interpretation and construction of $\mu$ , we have $\eta_{\mathcal{I}}(a)=\mu(d)$ iff $d=a^{\mathcal{I}}$ , and $\eta_{\mathcal{I}}(b)=\mu(e)$ iff $e=b^{\mathcal{I}}$ , and $(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$ . By the semantics of ${\cal ELH}$ , this means $\mathcal{I}\models r(a,b)$ . $\hfill\blacktriangleleft$

Lemma 52.

If $\mathcal{I_{\mathcal{O}}}$ is the canonical model of $\mathcal{O}$ , then the geometrical interpretation $\eta_{\mathcal{I}_{\mathcal{O}}}$ of ${\mathcal{I}_{\mathcal{O}}}$ is strongly IQ faithful with respect to $\mathcal{O}$ . That is, $\mathcal{O}\models\alpha$ iff $\eta_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ , where $\alpha$ is an ${\cal ELH}$ IQ.

Proof.

$\mathcal{I}_{\mathcal{O}}$ is canonical, therefore ${\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ . By Lemma 50 we have that $\mathcal{I}\models C(a)$ iff $\eta_{\mathcal{I}}\models C(a)$ , and by Lemma 51 we have that $\mathcal{I}\models r(a,b)$ iff $\eta_{\mathcal{I}}\models r(a,b)$ . This just means $\mathcal{I}\models\alpha$ iff $\eta_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ , giving us $\eta_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ . $\hfill\blacktriangleleft$

Lemma 53.

For all $C, D$ it is the case that $\mathcal{I}\models C\sqsubseteq D$ iff $\eta_{\mathcal{I}}\models C\sqsubseteq D$ .

Proof.

Let $C, D$ be $\mathcal{ELH}$ concepts. Assume $\mathcal{I}\models C\sqsubseteq D$ . By the semantics of $\mathcal{ELH}$ , this means $C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$ . Let $v\in\eta_{\mathcal{I}}(C)$ . By Lemma 47 we have that $v=\mu(d)\in\eta_{\mathcal{I}}(C)$ . We know, by Lemma 49, that $\mu(d)\in\eta_{\mathcal{I}}(C)$ iff $d\in C^{\mathcal{I}}$ . Since we have $d\in C^{\mathcal{I}}$ , we also have, by assumption, $d\in D^{\mathcal{I}}$ . Again by Lemma 49, this gives us $\mu(d)\in\eta_{\mathcal{I}}(D)$ . Since $d$ was chosen arbitrarily, this is the case iff $\eta_{\mathcal{I}}\models C\sqsubseteq D$ .

Now assume $\eta_{\mathcal{I}}\models C\sqsubseteq D$ . By the semantics of $\mathcal{ELH}$ , $\eta_{\mathcal{I}}(C)\subseteq\eta_{\mathcal{I}}(D)$ . Now assume $d\in C^{\mathcal{I}}$ . We know, by Lemma 49, that this is the case iff $\mu(d)\in\eta_{\mathcal{I}}(C)$ . By assumption, we get $\mu(d)\in\eta_{\mathcal{I}}(D)$ . Since $v$ was arbitrary, and we showed that $d\in C^{\mathcal{I}}$ implies $d\in D^{\mathcal{I}}$ , this means $\mathcal{I}\models C\sqsubseteq D$ . $\hfill\blacktriangleleft$

Lemma 54.

For all $r,s\in N_{R}$ , it is the case that $\mathcal{I}\models r\sqsubseteq s$ iff $\eta_{\mathcal{I}}\models r\sqsubseteq s$ .

Proof.

Assume $\mathcal{I}\models r\sqsubseteq s$ . B the semantics of $\mathcal{ELH}$ , $r^{\mathcal{I}}\subseteq s^{\mathcal{I}}$ . Now let $v=u\oplus w\in\eta_{\mathcal{I}}(r)$ . This means $v\in\{\mu(d)\oplus\mu(e)\mid(d,e)\in r^{\mathcal{I}}\}$ , and, by Lemma 48 there are $d,e\in\Delta^{\mathcal{I}}$ such that $u=\mu(d)$ , $w=\mu(e)$ and $(d,e)\in r^{\mathcal{I}}$ . By assumption, $(d,e)\in s^{\mathcal{I}}$ . By construction of $\mu$ , this means $\mu(d)[s,e]=1$ . Since we know $v=\mu(d)\oplus\mu(e)$ and $\mu(d)[s,e]=1$ , by the definition of $\eta_{\mathcal{I}}$ we have that $v\in\eta_{\mathcal{I}}(s)$ , and, therefore $\eta_{\mathcal{I}}\models r\sqsubseteq s$ .

Now assume $\eta_{\mathcal{I}}\models r\sqsubseteq s$ . By the semantics of $\mathcal{ELH}$ , this means $\eta_{\mathcal{I}}(r)\subseteq\eta_{\mathcal{I}}(s)$ . Let $(d,e)\in r^{\mathcal{I}}$ . By the construction of $\mu$ , this means $\mu(d)[r,e]=1$ . By the definition of $\eta_{\mathcal{I}}$ , there is $v=\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}(r)$ . By assumption, $v\in\eta_{\mathcal{I}}(s)$ . But, by Lemma 48, there are $d,e\in\Delta^{\mathcal{I}}$ such that $u=\mu(d)$ , $w=\mu(e)$ , and $(d,e)\in s^{\mathcal{I}}$ . Since we have proven $(d,e)\in r^{\mathcal{I}}$ implies $(d,e)\in s^{\mathcal{I}}$ , this means $\mathcal{I}\models r\sqsubseteq s$ . $\hfill\blacktriangleleft$

See 25

Proof.

When $\alpha$ is a concept inclusion, the result comes from Lemma 53. When $\alpha$ is a role inclusion, the result comes from Lemma 54. When $\alpha$ is an IQ, the result comes from Lemma 50 and from Lemma 51 $\hfill\blacktriangleleft$

See 27

Proof.

We divide the proof into claims, first for assertions and then for concept and role inclusions. In the following, let $\mathcal{O}=\mathcal{T}\cup\mathcal{A}$ be an ${\cal ELH}$ ontology in normal form, with $\mathcal{T}$ being the set of ${\cal ELH}$ concept and role inclusions in $\mathcal{O}$ and $\mathcal{A}$ being the set of ${\cal ELH}$ assertions in $\mathcal{O}$ . As mentioned before, $N_{C}(\mathcal{O})$ , $N_{R}(\mathcal{O})$ , and $N_{I}(\mathcal{A})$ denote the set of concept, role, and individual names occurring in $\mathcal{O}$ , respectively. In the following, let $A,A_{1},A_{2},B,B^{\prime}$ be arbitrary concept names in $N_{C}(\mathcal{O})$ , let $a, b$ be arbitrary individual names in $N_{I}(\mathcal{A})$ , and let $r,s,s^{\prime}$ be arbitrary role names in $N_{R}(\mathcal{O})$ .

Claim 55.

${\mathcal{I}_{\mathcal{O}}}\models A(a)$ iff $\mathcal{O}\models A(a)$ .

Proof.

Assume $\mathcal{O}\models A(a)$ . Now, by the definition of ${\mathcal{I}_{\mathcal{O}}}$ (Definition 26), it is the case that $A^{{\mathcal{I}_{\mathcal{O}}}}\supseteq\{a\in N_{I}(\mathcal{A})\mid\mathcal{% O}\models A(a)\}$ . By assumption, we have that $a\in A^{\mathcal{I}_{\mathcal{O}}}$ . But since $a\in N_{I}(\mathcal{A})$ , by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have $a^{\mathcal{I}_{\mathcal{O}}}=a$ and, therefore, $a^{\mathcal{I}_{\mathcal{O}}}\in A^{\mathcal{I}_{\mathcal{O}}}$ , which means ${\mathcal{I}_{\mathcal{O}}}\models A(a)$ .
Now assume ${\mathcal{I}_{\mathcal{O}}}\models A(a)$ . This means $a^{\mathcal{I}_{\mathcal{O}}}\in A^{\mathcal{I}_{\mathcal{O}}}$ . We know, by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , that $a^{\mathcal{I}_{\mathcal{O}}}=a$ . Also by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , we know $A^{\mathcal{I}_{\mathcal{O}}}$ = $\{a\in N_{I}(\mathcal{A})\,|\,\mathcal{O}\models A(a)\}$ $\cup$ $\{c_{D}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\,|\,\mathcal{O}\models D% \sqsubseteq A\}$ . Since $a\in N_{I}(\mathcal{A})$ , we have that $a\not\in\Delta^{{\mathcal{I}_{\mathcal{O}}}}_{u+}$ , and thus, $\mathcal{O}\models A(a)$ . $\hfill\vartriangleleft$

Claim 56.

${\mathcal{I}_{\mathcal{O}}}\models r(a,b)$ iff $\mathcal{O}\models r(a,b)$ .

Proof.

Assume $\mathcal{O}\models r(a,b)$ . By the definition of canonical model (Definition 26), $r^{\mathcal{I}_{\mathcal{O}}}\supseteq\{(a,b)\in N_{I}(\mathcal{A})\times N_{I% }(\mathcal{A})\mid\mathcal{O}\models r(a,b)\}$ . Since we assumed that $\mathcal{O}\models r(a,b)$ , we have that $(a,b)\in r^{\mathcal{I}_{\mathcal{O}}}$ . Now, again by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $a^{\mathcal{I}_{\mathcal{O}}}=a$ , and $b^{\mathcal{I}_{\mathcal{O}}}=b$ . This means $(a^{\mathcal{I}_{\mathcal{O}}},b^{\mathcal{I}_{\mathcal{O}}})\in r^{\mathcal{I% }_{\mathcal{O}}}$ , which is the case iff ${\mathcal{I}_{\mathcal{O}}}\models r(a,b)$ .
Now assume ${\mathcal{I}_{\mathcal{O}}}\models r(a,b)$ . Then, we know $(a^{\mathcal{I}_{\mathcal{O}}},b^{\mathcal{I}_{\mathcal{O}}})\in r^{\mathcal{I% }_{\mathcal{O}}}$ . By definition of $r^{\mathcal{I}_{\mathcal{O}}}$ , we have that $(a,b)\in r^{\mathcal{I}_{\mathcal{O}}}$ . Since $a,b\in N_{I}$ , by definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have $\mathcal{O}\models r(a,b)$ . $\hfill\vartriangleleft$

Claim 57.

${\mathcal{I}_{\mathcal{O}}}\models\exists r.A(a)$ iff $\mathcal{O}\models\exists r.A(a)$ .

Proof.

Assume $\mathcal{O}\models\exists r.A(a)$ . By the definition of ${\mathcal{I}_{\mathcal{O}}}$ (Definition 26), we have $r^{\mathcal{I}_{\mathcal{O}}}\supseteq\{(a,c_{A})\in N_{I}(\mathcal{A})\times% \Delta^{\mathcal{I}_{\mathcal{O}}}\mid\mathcal{O}\models\exists r.A(a)\}$ . This means $(a,c_{A})\in r^{\mathcal{I}_{\mathcal{O}}}$ . Also, by the definition of the canonical model, $a^{\mathcal{I}_{\mathcal{O}}}=a$ and $c_{A}\in A^{\mathcal{I}_{\mathcal{O}}}$ , and therefore $a^{\mathcal{I}_{\mathcal{O}}}\in(\exists r.A)^{\mathcal{I}_{\mathcal{O}}}$ . This gives us ${\mathcal{I}_{\mathcal{O}}}\models\exists r.A(a)$ .
Now assume ${\mathcal{I}_{\mathcal{O}}}\models\exists r.A(a)$ . Then, $a^{\mathcal{I}_{\mathcal{O}}}\in(\exists r.A)^{\mathcal{I}_{\mathcal{O}}}$ . By the definition of the canonical model, either (1) there is $b\in N_{I}(\mathcal{A})$ such that $(a,b)\in r^{\mathcal{I}_{\mathcal{O}}}$ and $b\in A^{\mathcal{I}_{\mathcal{O}}}$ or (2) there is $c_{A^{\prime}}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$ such $(a,c_{A^{\prime}})\in r^{\mathcal{I}_{\mathcal{O}}}$ and $c_{A^{\prime}}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . In case (1), by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $(a,b)\in r^{\mathcal{I}_{\mathcal{O}}}$ means that $\mathcal{O}\models r(a,b)$ . We also have that it is the case that $b\in A^{\mathcal{I}_{\mathcal{O}}}$ . By the definition of the canonical model, this means that $b\in\{b\in N_{I}(\mathcal{A})\mid\mathcal{O}\models A(b)\}$ , so $\mathcal{O}\models A(b)$ . By the semantics of $\mathcal{ELH}$ , $\mathcal{O}\models r(a,b)$ and $\mathcal{O}\models A(b)$ implies $\mathcal{O}\models\exists r.A(a)$ . In case (2), by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(a,c_{A^{\prime}})\in r^{\mathcal{I}_{\mathcal{O}}}$ means that $\mathcal{O}\models\exists r.A^{\prime}(a)$ . Again by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , $c_{A^{\prime}}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ implies $\mathcal{T}\models{A^{\prime}}\sqsubseteq A$ . This gives us $\mathcal{O}\models\exists r.A(a)$ . $\hfill\vartriangleleft$

Claim 58.

${\mathcal{I}_{\mathcal{O}}}\models A_{1}\sqcap A_{2}\sqsubseteq B$ iff $\mathcal{O}\models A_{1}\sqcap A_{2}\sqsubseteq B$ .

Proof.

Assume $\mathcal{O}\models A_{1}\sqcap A_{2}\sqsubseteq B$ . We make a case distinction based on the elements in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}:=N_{I}(\mathcal{A})\cup\Delta^{\mathcal{I% }_{\mathcal{O}}}_{u+}$ .

$\blacksquare$

$a\in N_{I}(\mathcal{A})$ : Assume $a\in(A_{1}\sqcap A_{2})^{\mathcal{I}_{\mathcal{O}}}$ . This is the case iff $a\in A_{1}^{\mathcal{I}_{\mathcal{O}}}$ and $a\in A_{2}^{\mathcal{I}_{\mathcal{O}}}$ . By the definition of ${\mathcal{I}_{\mathcal{O}}}$ , this means $\mathcal{O}\models A_{1}(a)$ and $\mathcal{O}\models A_{2}(a)$ . By assumption, this gives us $\mathcal{O}\models B(a)$ , which, by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , means that $a\in B^{\mathcal{I}_{\mathcal{O}}}$ . Therefore, ${\mathcal{I}_{\mathcal{O}}}\models B(a)$ . Since $a$ was an arbitrary element in $N_{I}(\mathcal{A})$ , this holds for all elements of this kind.
$\blacksquare$

$c_{D}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$ : Assume $c_{D}\in(A_{1}\sqcap A_{2})^{\mathcal{I}_{\mathcal{O}}}$ . This means $c_{D}\in A_{1}^{\mathcal{I}_{\mathcal{O}}}$ and $c_{D}\in A_{2}^{\mathcal{I}_{\mathcal{O}}}$ . By the definition of ${\mathcal{I}_{\mathcal{O}}}$ , this gives us that $\mathcal{T}\models D\sqsubseteq A_{1}$ and $\mathcal{T}\models D\sqsubseteq A_{2}$ . By assumption, this means $\mathcal{T}\models D\sqsubseteq B$ . But, by the definition of ${\mathcal{I}_{\mathcal{O}}}$ , this means $c_{D}\in B^{\mathcal{I}_{\mathcal{O}}}$ . Since $c_{D}$ was an arbitrary element in $\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$ , this argument can be applied for all elements of this kind.

We have thus shown that, for all elements $d$ in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}$ , if $d\in(A_{1}\sqcap A_{2})^{{\mathcal{I}_{\mathcal{O}}}}$ then $d\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . So ${\mathcal{I}_{\mathcal{O}}}\models A_{1}\sqcap A_{2}\sqsubseteq B$ .
Now, assume $\mathcal{O}\not\models A_{1}\sqcap A_{2}\sqsubseteq B$ . We show that ${\mathcal{I}_{\mathcal{O}}}\not\models A_{1}\sqcap A_{2}\sqsubseteq B$ by showing that $c_{A_{1}\sqcap A_{2}}\in(A_{1}\sqcap A_{2})^{{\mathcal{I}_{\mathcal{O}}}}$ but $c_{A_{1}\sqcap A_{2}}\not\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , $c_{A_{1}\sqcap A_{2}}\in A^{{\mathcal{I}_{\mathcal{O}}}}_{i}$ since $\mathcal{T}\models A_{1}\sqcap A_{2}\sqsubseteq A_{i}$ (trivially), where $i\in\{1,2\}$ . Then, by the semantics of ${\cal ELH}$ , $c_{A_{1}\sqcap A_{2}}\in(A_{1}\sqcap A_{2})^{{\mathcal{I}_{\mathcal{O}}}}$ . We now argue that $c_{A_{1}\sqcap A_{2}}\not\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . This follows again by the definition of ${\mathcal{I}_{\mathcal{O}}}$ and the assumption that $\mathcal{O}\not\models A_{1}\sqcap A_{2}\sqsubseteq B$ , since the definition means that $c_{D}\not\in B^{{\mathcal{I}_{\mathcal{O}}}}$ iff $\mathcal{O}\models D\sqsubseteq B$ and we can take $D=A_{1}\sqcap A_{2}$ . $\hfill\vartriangleleft$

Claim 59.

${\mathcal{I}_{\mathcal{O}}}\models\exists r.B\sqsubseteq A$ iff $\mathcal{O}\models\exists r.B\sqsubseteq A$ .

Proof.

Assume $\mathcal{O}\models\exists r.B\sqsubseteq A$ . We make a case distinction based on the elements in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}:=N_{I}(\mathcal{A})\cup\Delta^{\mathcal{I% }_{\mathcal{O}}}_{u+}$ .

$\blacksquare$

$a\in N_{I}(\mathcal{A})$ : Assume $a\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . In this case, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , either (1) there is $b\in N_{I}(\mathcal{A})$ such that $(a,b)\in r^{{\mathcal{I}_{\mathcal{O}}}}$ and $b\in B^{{\mathcal{I}_{\mathcal{O}}}}$ or (2) there is $c_{B^{\prime}}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$ such that $(a,c_{B^{\prime}})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ and $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . In case (1), by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(a,b)\in r^{{\mathcal{I}_{\mathcal{O}}}}$ implies that $\mathcal{O}\models r(a,b)$ . Also, $b\in B^{{\mathcal{I}_{\mathcal{O}}}}$ implies that $\mathcal{O}\models B(b)$ . Together with the assumption that $\mathcal{O}\models\exists r.B\sqsubseteq A$ , this means that $\mathcal{O}\models A(a)$ . Again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $a\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . In case (2), by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(a,c_{B^{\prime}})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ implies that $\mathcal{O}\models\exists r.B^{\prime}(a)$ . Also, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ implies that $\mathcal{T}\models B^{\prime}\sqsubseteq B$ . Then, $\mathcal{O}\models\exists r.B(a)$ . By assumption $\mathcal{O}\models\exists r.B\sqsubseteq A$ , which means that $\mathcal{O}\models A(a)$ . Again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $a\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $a$ was an arbitrary element in $N_{I}(\mathcal{A})$ , this argument can be applied for all elements of this kind.
$\blacksquare$

$c_{D}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$ : Assume $c_{D}\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . In this case, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , either (1) there is $c_{B^{\prime}}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$ such that $(c_{D},c_{B^{\prime}})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ and $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ or (2) $D$ is of the form $\exists s.B^{\prime}$ , $(c_{D},c_{B^{\prime}})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ , $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ , and $\mathcal{T}\models s\sqsubseteq r$ . In case (1), by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $\mathcal{T}\models D\sqsubseteq A$ and $\mathcal{T}\models A\sqsubseteq\exists r.B^{\prime}$ . Again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ implies $\mathcal{T}\models B^{\prime}\sqsubseteq B$ . This means that $\mathcal{T}\models D\sqsubseteq\exists r.B$ . By assumption $\mathcal{O}\models\exists r.B\sqsubseteq A$ , which means $\mathcal{T}\models\exists r.B\sqsubseteq A$ . Then, $\mathcal{T}\models D\sqsubseteq A$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $c_{D}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . In case (2), we have that $\mathcal{T}\models D\sqsubseteq\exists r.B^{\prime}$ since $D$ is of the form $\exists s.B^{\prime}$ and $\mathcal{T}\models s\sqsubseteq r$ . Also, as $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ , by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $\mathcal{T}\models B^{\prime}\sqsubseteq B$ . Then, $\mathcal{T}\models D\sqsubseteq\exists r.B$ . By assumption, $\mathcal{O}\models\exists r.B\sqsubseteq A$ , which then means that $\mathcal{T}\models D\sqsubseteq A$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $c_{D}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $c_{D}$ was an arbitrary element in $\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$ , this argument can be applied for all elements of this kind.

We have thus shown that, for all elements $d$ in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}$ , if $d\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ then $d\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . So ${\mathcal{I}_{\mathcal{O}}}\models\exists r.B\sqsubseteq A$ .
Now, assume $\mathcal{O}\not\models\exists r.B\sqsubseteq A$ . We show that ${\mathcal{I}_{\mathcal{O}}}\not\models\exists r.B\sqsubseteq A$ by showing that $c_{\exists r.B}\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ but $c_{\exists r.B}\not\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . By the definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(c_{\exists s.B},c_{B})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ if $\mathcal{T}\models s\sqsubseteq r$ , which is trivially the case for $s=r$ , and $c_{B}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ by definition of ${\mathcal{I}_{\mathcal{O}}}$ . We now argue that $c_{\exists r.B}\not\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , an element of the form $c_{D}$ is in $A^{{\mathcal{I}_{\mathcal{O}}}}$ iff $\mathcal{T}\models D\sqsubseteq A$ . By assumption $\mathcal{O}\not\models\exists r.B\sqsubseteq A$ which means $\mathcal{T}\not\models\exists r.B\sqsubseteq A$ . So $c_{\exists r.B}$ is not in $A^{{\mathcal{I}_{\mathcal{O}}}}$ . $\hfill\vartriangleleft$

Claim 60.

${\mathcal{I}_{\mathcal{O}}}\models A\sqsubseteq\exists r.B$ iff $\mathcal{O}\models A\sqsubseteq\exists r.B$ .

Proof.

Assume $\mathcal{O}\models A\sqsubseteq\exists r.B$ . We make a case distinction based on the elements in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}:=N_{I}(\mathcal{A})\cup\Delta^{\mathcal{I% }_{\mathcal{O}}}_{u+}$ .

$\blacksquare$

$a\in N_{I}(\mathcal{A})$ : Assume $a\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have $\mathcal{O}\models A(a)$ . By assumption $\mathcal{O}\models A\sqsubseteq\exists r.B$ , so $\mathcal{O}\models\exists r.B(a)$ . Then, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(a,c_{B})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ . Again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have $c_{B}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . So $a\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $a$ was an arbitrary element in $N_{I}(\mathcal{A})$ , the argument golds for all similar elements.
$\blacksquare$

$c_{D}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$ : Assume $c_{D}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $\mathcal{T}\models D\sqsubseteq A$ . By assumption, $\mathcal{O}\models A\sqsubseteq\exists r.B$ which means $\mathcal{T}\models A\sqsubseteq\exists r.B$ . Then, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(c_{D},c_{B})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ . Again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $c_{B}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . So $c_{D}\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $c_{D}$ was an arbitrary element in $\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}$ , this argument holds for all similar elements.

We have thus shown that, for all elements $d$ in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}$ , if $d\in A^{{\mathcal{I}_{\mathcal{O}}}}$ then $d\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . This means that ${\mathcal{I}_{\mathcal{O}}}\models A\sqsubseteq\exists r.B$ .
Now, assume $\mathcal{O}\not\models A\sqsubseteq\exists r.B$ . We show that ${\mathcal{I}_{\mathcal{O}}}\not\models A\sqsubseteq\exists r.B$ by showing that $c_{A}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ but $c_{A}\not\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $\{c_{D}\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\,|\,\mathcal{T}\models D% \sqsubseteq A\}\subseteq A^{{\mathcal{I}_{\mathcal{O}}}}$ . For $D=A$ we trivially have that $\mathcal{T}\models A\sqsubseteq A$ , so $c_{A}\in A^{{\mathcal{I}_{\mathcal{O}}}}$ . We now show that $c_{A}\not\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ . Suppose this is not the case and there is some element $d\in\Delta^{{\mathcal{I}_{\mathcal{O}}}}$ such that $(c_{A},d)\in r^{{\mathcal{I}_{\mathcal{O}}}}$ and $d\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , this can happen iff $d$ is of the form $c_{B^{\prime}}$ in $\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$ and, moreover, $\mathcal{T}\models A\sqsubseteq A^{\prime}\text{ and }\mathcal{T}\models A^{% \prime}\sqsubseteq\exists r.B^{\prime}$ for some $A^{\prime}\in N_{C}(\mathcal{O})$ . We now argue $d=c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ implies $\mathcal{T}\models B^{\prime}\sqsubseteq B$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , $c_{B^{\prime}}\in B^{{\mathcal{I}_{\mathcal{O}}}}$ iff $\mathcal{T}\models B^{\prime}\sqsubseteq B$ . Since $\mathcal{T}\models A\sqsubseteq A^{\prime}\text{ and }\mathcal{T}\models A^{% \prime}\sqsubseteq\exists r.B^{\prime}$ , we have $\mathcal{T}\models A\sqsubseteq\exists r.B$ , which means $\mathcal{O}\models A\sqsubseteq\exists r.B$ . This contradicts our assumption that there is some element $d\in\Delta^{{\mathcal{I}_{\mathcal{O}}}}$ such that $(c_{A},d)\in r^{{\mathcal{I}_{\mathcal{O}}}}$ and $d\in B^{{\mathcal{I}_{\mathcal{O}}}}$ . Thus, $c_{A}\not\in(\exists r.B)^{{\mathcal{I}_{\mathcal{O}}}}$ , as required. $\hfill\vartriangleleft$

Claim 61.

${\mathcal{I}_{\mathcal{O}}}\models r\sqsubseteq s$ iff $\mathcal{O}\models r\sqsubseteq s$ .

Proof.

Assume $\mathcal{O}\models r\sqsubseteq s$ . We make a case distinction based on the elements in $\Delta^{{\mathcal{I}_{\mathcal{O}}}}$ and how they can be related in the extension of a role name in the definition of ${\mathcal{I}_{\mathcal{O}}}$ .

$\blacksquare$

$(a,b)\in N_{I}(\mathcal{A})\times N_{I}(\mathcal{A})$ : Assume $(a,b)\in r^{{\mathcal{I}_{\mathcal{O}}}}$ . We first argue that in this case $\mathcal{O}\models r(a,b)$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , $(a,b)\in r^{{\mathcal{I}_{\mathcal{O}}}}\text{ iff }\mathcal{O}\models r(a,b)$ . Since by assumption $\mathcal{O}\models r\sqsubseteq s$ we have that $\mathcal{O}\models s(a,b)$ , so $(a,b)\in s^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $(a,b)$ was an arbitrary pair in $N_{I}(\mathcal{A})\times N_{I}(\mathcal{A})$ , the argument can be applied for all such kinds of pairs.
$\blacksquare$

$(a,c_{B})\in N_{I}(\mathcal{A})\times\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$ : Assume $(a,c_{B})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ . We first argue that in this case $\mathcal{O}\models\exists r.B(a)$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $(a,c_{B})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ iff $\mathcal{O}\models\exists r.B(a)$ . By assumption $\mathcal{O}\models r\sqsubseteq s$ . So $\mathcal{O}\models\exists s.B(a)$ . Then, again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $(a,c_{B})\in s^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $(a,c_{B})$ was an arbitrary pair in $N_{I}(\mathcal{A})\times\Delta^{\mathcal{I}_{\mathcal{O}}}_{u}$ , this argument can be applied for all such kinds of pairs.
$\blacksquare$

$(c_{D},c_{B})\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\times\Delta^{\mathcal{% I}_{\mathcal{O}}}_{u}$ : Assume $(c_{D},c_{B})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ . In this case, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , either (1) $\mathcal{T}\models D\sqsubseteq A\text{ and }\mathcal{T}\models A\sqsubseteq% \exists r.B$ , for some $A\in N_{C}(\mathcal{O})$ , or (2) $D$ is of the form $\exists s^{\prime}.B$ and $\mathcal{T}\models s^{\prime}\sqsubseteq r$ . In case (1), since by assumption $\mathcal{O}\models r\sqsubseteq s$ , we have that $\mathcal{T}\models D\sqsubseteq A\text{ and }\mathcal{T}\models A\sqsubseteq% \exists s.B$ , for some $A\in N_{C}(\mathcal{O})$ . Then, by definition of ${\mathcal{I}_{\mathcal{O}}}$ , it follows that $(c_{D},c_{B})\in s^{{\mathcal{I}_{\mathcal{O}}}}$ . In case (2), since $\mathcal{T}\models s^{\prime}\sqsubseteq r$ and by assumption $\mathcal{O}\models r\sqsubseteq s$ (which means $\mathcal{T}\models r\sqsubseteq s$ ), we have that $\mathcal{T}\models s^{\prime}\sqsubseteq s$ . Then, again by definition of ${\mathcal{I}_{\mathcal{O}}}$ , as in this case $D$ is of the form $\exists s^{\prime}.B$ , it follows that $(c_{D},c_{B})\in s^{{\mathcal{I}_{\mathcal{O}}}}$ . Since $(c_{D},c_{B})$ was an arbitrary pair in $\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\times\Delta^{\mathcal{I}_{\mathcal{O}}% }_{u}$ , this argument can be applied for all such kinds of pairs.

We have thus shown that ${\mathcal{I}_{\mathcal{O}}}\models r\sqsubseteq s$ .
Now, assume $\mathcal{O}\not\models r\sqsubseteq s$ . We show that ${\mathcal{I}_{\mathcal{O}}}\not\models r\sqsubseteq s$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , we have that $\{(c_{\exists s.B},c_{B})\in\Delta^{\mathcal{I}_{\mathcal{O}}}_{u+}\times% \Delta^{\mathcal{I}_{\mathcal{O}}}_{u}\mid\mathcal{T}\models s\sqsubseteq r\}% \subseteq r^{{\mathcal{I}_{\mathcal{O}}}}$ . By taking $B=\top$ and $s=r$ (and since trivially $\mathcal{T}\models r\sqsubseteq r$ ), we have in particular that $(c_{\exists r.\top},c_{\top})\in r^{{\mathcal{I}_{\mathcal{O}}}}$ . We now argue that $(c_{\exists r.\top},c_{\top})\notin s^{{\mathcal{I}_{\mathcal{O}}}}$ . By definition of ${\mathcal{I}_{\mathcal{O}}}$ , a pair of the form $(c_{\exists s^{\prime}.B},c_{B})$ is in $s^{{\mathcal{I}_{\mathcal{O}}}}$ iff $\mathcal{T}\models s^{\prime}\sqsubseteq s$ . By assumption $\mathcal{O}\not\models r\sqsubseteq s$ , which means $\mathcal{T}\not\models r\sqsubseteq s$ . So the pair $(c_{\exists r.\top},c_{\top})$ is not in $s^{{\mathcal{I}_{\mathcal{O}}}}$ . $\hfill\vartriangleleft$

This finishes our proof. $\hfill\blacktriangleleft$

Lemma 62.

Let $\mathcal{O}$ be a normalized ${\cal ELH}$ ontology and let ${\mathcal{I}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (Definition 26). The ${\mathsf{d}}$ -dimensional $\oplus$ -geometric interpretation of ${\mathcal{I}_{\mathcal{O}}}$ (Definition 21) is a strongly TBox faithful model of $\mathcal{O}$ .

Proof.

From Theorem 27, if $\tau$ is an ${\cal ELH}$ CI in normal form or an ${\cal ELH}$ role inclusion over ${\sf sig}(\mathcal{O})$ , then ${\mathcal{I}_{\mathcal{O}}}\models\tau$ iff $\mathcal{O}\models\tau$ . Since, by Lemma 53 it is the case that $\mathcal{I}\models C\sqsubseteq D$ iff $\eta_{\mathcal{I}}\models C\sqsubseteq D$ (where $C$ and $D$ are arbitrary ${\cal ELH}$ concepts) and by Lemma 54 it is the case that $\mathcal{I}\models r\sqsubseteq s$ iff $\eta_{\mathcal{I}}\models r\sqsubseteq s$ (with $r,s\in{\sf N_{R}}$ ), we have that $\mathcal{I}\models\tau$ iff $\eta_{\mathcal{I}_{\mathcal{O}}}\models\tau$ , where $\tau$ is a TBox axiom in normal form. This gives us $\eta_{\mathcal{I}_{\mathcal{O}}}\models\tau$ iff $\mathcal{O}\models\tau$ for any normalized TBox axiom. $\hfill\blacktriangleleft$

See 28

Proof.

This result follows from Lemmas 52 and 62. $\hfill\blacktriangleleft$

Lemma 63.

For all $r\in N_{R}$ , all $a,b\in N_{I}$ , it is the case that $\eta_{\mathcal{I}}\models r(a,b)$ iff $\eta_{\mathcal{I}}^{*}\models r(a,b)$ .

Proof.

We know that $\eta_{\mathcal{I}}^{*}\models r(a,b)$ iff it is true that $\eta_{\mathcal{I}}^{*}(a)\oplus\eta_{\mathcal{I}}^{*}(b)\in\eta_{\mathcal{I}}^% {*}(r)$ . From the definition of $\eta_{\mathcal{I}}^{*}$ we know $\eta_{\mathcal{I}}^{*}(a)\oplus\eta_{\mathcal{I}}^{*}(b)=\eta_{\mathcal{I}}(a)% \oplus\eta_{\mathcal{I}}(b)$ . Since $\mu(d)$ is binary for any $d$ , we have $\eta_{\mathcal{I}}(a)\oplus\eta_{\mathcal{I}}(b)$ is binary. From Corollary 7, we have $\eta_{\mathcal{I}}(a)\oplus\eta_{\mathcal{I}}(b)\in\eta_{\mathcal{I}}(r)$ , which, by the definition of satisfaction is the case iff $\eta_{\mathcal{I}}\models r(a,b)$ . $\hfill\blacktriangleleft$

Lemma 64.

For any vector $v$ , such that $v$ is a result of the mapping in Definition 19, if $v\in\eta_{\mathcal{I}}^{*}(A)$ , then $v[A]=1$ .

Proof.

By the definition of $\eta_{\mathcal{I}}^{*}$ and that of convex hull, for all $v$ , it holds that $v\in\eta_{\mathcal{I}}^{*}(A)$ means $\exists$ $\lambda_{i}0\leq\lambda_{i}\leq 1$ such that $v=\sum_{i=1}^{n}v_{i}\lambda_{i}$ , with $v_{i}\in\eta_{\mathcal{I}}(A)$ . By the definition of $\eta_{\mathcal{I}}$ , it is true that $v_{i}\in\eta_{\mathcal{I}}(A)$ is the case iff $v_{i}[A]=1$ , for all $1\leq i\leq n$ . By the definition of convex hull, this means $v[A]=1$ . $\hfill\blacktriangleleft$

Lemma 65.

For all $\mathcal{ELH}$ IQs in normal form $\alpha$ , it is the case that $\eta_{\mathcal{I}}^{*}\models\alpha$ iff $\eta_{\mathcal{I}}\models\alpha$ .

Proof.

If $\alpha$ is a role assertion the Lemma follows from Lemma 63. Now, we will consider the remaining cases. Let $A,B\in N_{C}$ be concept names, and $a\in N_{I}$ be an individual name. We make a case distinction and divide the proof into claims for readability.

Claim 66.

Case 1: $\eta_{\mathcal{I}}^{*}\models A(a)$ iff $\eta_{\mathcal{I}}\models A(a)$ .

Proof.

Assume $\eta_{\mathcal{I}}^{*}\models A(a)$ . By the semantics of geometric interpretation, $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(A)$ . By the definition of $\mu$ , it is the case that $\eta_{\mathcal{I}}^{*}(a)$ is binary and, by the definition of $\eta_{\mathcal{I}}^{*}$ , it is the case that $\eta_{\mathcal{I}}^{*}(a)=\eta_{\mathcal{I}}(a)$ . From Corollary 7 we get that $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(A)$ , which is the case iff $\eta_{\mathcal{I}}\models A(a)$ .
Now assume $\eta_{\mathcal{I}}\models A(a)$ . This means $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(A)$ . By definition of $\eta_{\mathcal{I}}^{*}$ , we know $\eta_{\mathcal{I}}(a)=\eta_{\mathcal{I}}^{*}(a)$ , and by Proposition 5 we know $\eta_{\mathcal{I}}(A)\subseteq\eta_{\mathcal{I}}^{*}(A)$ . By assumption, $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(A)$ . By the semantics of geometric interpretation, this means $\eta_{\mathcal{I}}^{*}\models A(a)$ . $\hfill\vartriangleleft$

Claim 67.

Case 2: $\eta_{\mathcal{I}}^{*}\models(\exists r.A(a))$ iff $\eta_{\mathcal{I}}\models(\exists r.A(a))$ .

Proof.

Assume $\eta_{\mathcal{I}}^{*}\models\exists r.A(a)$ . By the semantics of $\eta_{\mathcal{I}}^{*}$ , we have that $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(\exists r.A)$ . By the definition of $\eta_{\mathcal{I}}^{*}$ , we know $\eta_{\mathcal{I}}^{*}(a)=\eta_{\mathcal{I}}(a)$ . Also, by construction of $\mu$ , it is the case that $\eta_{\mathcal{I}}(a)$ is binary. If there is a binary $v\in\eta_{\mathcal{I}}^{*}(A)$ such that $\eta_{\mathcal{I}}^{*}(a)\oplus v\in\eta_{\mathcal{I}}^{*}(r)$ then we are done. In this case, by Corollary 7, we have that $v\in\eta_{\mathcal{I}}(A)$ and $\eta_{\mathcal{I}}(a)\oplus v\in\eta_{\mathcal{I}}(r)$ . This means, by the semantics of $\eta_{\mathcal{I}}$ , that $\eta_{\mathcal{I}}\models\exists r.A(a)$ .
Otherwise, for all $v\in\eta_{\mathcal{I}}^{*}(A)$ such that $\eta_{\mathcal{I}}^{*}(a)\oplus v\in\eta_{\mathcal{I}}^{*}(r)$ we have that $v$ is non-binary (and, moreover, such $v$ exists). We rename this vector to $z$ , giving us $z=\eta_{\mathcal{I}}^{*}(a)\oplus v\in\eta_{\mathcal{I}}^{*}(r)$ . This means that $z=\sum_{i=1}^{n^{\prime}}v^{\prime}_{i}\lambda^{\prime}_{i}$ , such that $\exists\lambda^{\prime}_{i}$ with $0\leq\lambda^{\prime}_{i}\leq 1$ and $\sum_{i=1}^{n^{\prime}}\lambda^{\prime}_{i}=1$ , and it also means that $v^{\prime}_{1},\ldots,v^{\prime}_{n^{\prime}}\in\eta_{\mathcal{I}}(r)$ . For clarity, we call the vector on the left-hand side of the concatenation operation its prefix $\mathsf{pref}(x)$ , and the one on the right-hand side its suffix $\mathsf{suf}(x)$ . For example, regarding the vector $z\in\mathbb{R}^{2\cdot{\mathsf{d}}}$ renamed above, we have $\mathsf{pref}(z)=\eta_{\mathcal{I}}^{*}(a)\in\mathbb{R}^{{\mathsf{d}}}$ and $\mathsf{suf}(z)=v\in\mathbb{R}^{{\mathsf{d}}}$ .

We now need to demonstrate that $z\in\eta_{\mathcal{I}}(\exists r.A(a))$ . We show that (1) $\mathsf{pref}(z)[a]=1$ , (2) $\mathsf{pref}(z)[r,e]=1$ , and (3) $\mathsf{suf}(z)[A]=1$ .

1.

We now argue that, for any $v^{\prime}_{i}\in\eta_{\mathcal{I}}(r)$ such that $\sum_{i=1}^{n}v^{\prime}_{i}\lambda^{\prime}_{i}$ = $z$ , it must be the case that $\mathsf{pref}(v^{\prime}_{i})=\eta_{\mathcal{I}}^{*}(a)$ . This is because $\eta_{\mathcal{I}}^{*}(a)$ cannot be written as a convex combination of vectors $w^{\prime}\in(\eta_{\mathcal{I}}(r)\setminus\{\eta_{\mathcal{I}}^{*}(a)\oplus v% \mid v\in\mathbb{R}^{{\mathsf{d}}}\})$ such that $\mathsf{pref}(v^{\prime}_{i})=\sum_{i=1}^{n}w^{\prime}_{i}\lambda_{k}$ . If this was the case, every $w^{\prime}$ would have $\mathsf{pref}(w^{\prime})[a]=0$ , which, multiplied by any $\lambda^{\prime}_{i}$ , would of course still result in $\mathsf{pref}(w^{\prime})[a]=0$ , contradicting the fact that $z=\eta_{\mathcal{I}}^{*}(a)\oplus v$ . Since we know $\mathsf{pref}(z)=\eta_{\mathcal{I}}^{*}(a)$ , we have that $\mathsf{pref}(z)[a]=1$ .
2.

We now argue that $\mathsf{pref}(z)[r,e]=1$ . By Lemma 48, we know that, for $v^{\prime}_{i}\in\eta_{\mathcal{I}}(r)$ , there are $d,e\in\Delta^{\mathcal{I}}$ such that $\mathsf{pref}(v^{\prime}_{i})=\mu(d)$ , $\mathsf{suf}(v^{\prime}_{i})=\mu(e)$ , and $(d,e)\in r^{\mathcal{I}}$ , which, by the definition of $\mu$ , gives us $\mathsf{pref}(v^{\prime}_{i})[r,e]=1$ .
3.

From the fact we have assumed $v\in\eta_{\mathcal{I}}^{*}(A)$ and $v=\mathsf{suf}(z)$ , we know that $\mathsf{suf}(z)=\sum_{i=1}^{n}v_{i}\lambda_{i}$ with $v_{i}\in\eta_{\mathcal{I}}(A)$ . As $v\in\eta_{\mathcal{I}}^{*}(A)$ , we get from Lemma 64 that $\mathsf{suf}(z)[A]=1$ .

From these facts, we have that for $z=\sum_{i=1}^{n}v^{\prime}_{i}\lambda^{\prime}_{i}$ , it is true that $\mathsf{pref}(z)[a]=1$ , that $\mathsf{pref}(z)[r,e]=1$ , and that $\mathsf{suf}(z)[A]=1$ . By definition of $\eta_{\mathcal{I}}$ , this means $\mathsf{pref}(z)=\eta_{\mathcal{I}}(a)$ , that $z\in\eta_{\mathcal{I}}(r)$ , and that $\mathsf{suf}(z)=v\in\eta_{\mathcal{I}}(A)$ . Finally, by the semantics of $\eta_{\mathcal{I}}$ , we have $\eta_{\mathcal{I}}\models\exists r.A(a)$ .
Now assume $\eta_{\mathcal{I}}\models\exists r.A(a)$ . By the semantics of $\eta_{\mathcal{I}}$ , this means $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(\exists r.A)$ . We know, by the definition of $\eta_{\mathcal{I}}^{*}$ , that $\eta_{\mathcal{I}}(a)$ = $\eta_{\mathcal{I}}^{*}(a)$ , and therefore it is binary. Now, $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}(\exists r.A)$ means $\eta_{\mathcal{I}}^{*}(a)\oplus v\in\eta_{\mathcal{I}}(r)$ and $v\in\eta_{\mathcal{I}}(A)$ . Since $\eta_{\mathcal{I}}^{*}(a)\oplus v\in\eta_{\mathcal{I}}(r)$ , this means it is a binary vector, and by Proposition 5, it gives us $\eta_{\mathcal{I}}^{*}(a)\oplus v\in\eta_{\mathcal{I}}^{*}(r)$ . Since $v$ itself is binary and $v\in\eta_{\mathcal{I}}(A)$ , again by Proposition 5, we have $v\in\eta_{\mathcal{I}}^{*}(A)$ . This means, by the semantics of $\eta_{\mathcal{I}}^{*}$ , that $\eta_{\mathcal{I}}^{*}\models\exists r.A(a)$ .

Claim 68.

Case 3: $\eta_{\mathcal{I}}^{*}\models A\sqcap B(a)$ iff $\eta_{\mathcal{I}}\models A\sqcap B(a)$

Assume $\eta_{\mathcal{I}}^{*}\models A\sqcap B(a)$ . By the semantics of geometric interpretation, this means $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(A)$ and $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(B)$ . By the definition of $\eta_{\mathcal{I}}^{*}$ , it is the case that $\eta_{\mathcal{I}}^{*}(a)=\eta_{\mathcal{I}}(a)$ , and it is therefore binary. But, by Corollary 7 this means $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(A)$ and $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(B)$ . This means $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(A)\cap\eta_{\mathcal{I}}(B)$ , which gives us $\eta_{\mathcal{I}}\models A\sqcap B(a)$ .

Now assume $\eta_{\mathcal{I}}\models A\sqcap B(a)$ . This means $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(A)$ and $\eta_{\mathcal{I}}(a)\in\eta_{\mathcal{I}}(B)$ . By definition of $\eta_{\mathcal{I}}^{*}$ we have $\eta_{\mathcal{I}}(a)=\eta_{\mathcal{I}}^{*}(a)$ , and by Proposition 5 we have $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(A)$ and $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(B)$ . This means $\eta_{\mathcal{I}}^{*}(a)\in\eta_{\mathcal{I}}^{*}(A)\sqcap\eta_{\mathcal{I}}^% {*}(B)$ , giving us $\eta_{\mathcal{I}}^{*}\models A\sqcap B(a)$ . $\hfill\vartriangleleft$ This finishes our proof. $\hfill\blacktriangleleft$

Lemma 69.

Let $\mathcal{O}$ be a normalized ${\cal ELH}$ ontology and ${\mathcal{I}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ . The geometrical interpretation $\eta^{\ast}_{\mathcal{I}_{\mathcal{O}}}$ of ${\mathcal{I}_{\mathcal{O}}}$ is strongly IQ faithful with respect to $\mathcal{O}$ . That is, $\mathcal{O}\models\alpha$ iff $\eta^{\ast}_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ , where $\alpha$ is an ${\cal ELH}$ IQ in normal form.

Proof.

Since ${\mathcal{I}_{\mathcal{O}}}$ is canonical, ${\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ . By Lemma 52, we know $\mathcal{O}\models\alpha$ iff $\eta_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ . By Lemma 65, we have that if $\alpha$ is an ${\cal ELH}$ IQ in normal form then $\eta_{\mathcal{I}}\models\alpha$ iff $\eta_{\mathcal{I}}^{*}\models\alpha$ . This means $\eta_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\eta^{\ast}_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ . Hence, $\eta^{\ast}_{\mathcal{I}_{\mathcal{O}}}\models\alpha$ iff $\mathcal{O}\models\alpha$ . $\hfill\blacktriangleleft$

Lemma 70.

For all $C, D$ , it is the case that $\mathcal{I}\models C\sqsubseteq D$ iff $\eta_{\mathcal{I}}^{*}\models C\sqsubseteq D$ , where $C\sqsubseteq D$ is a TBox axiom.

Proof.

Let $C, D$ be $\mathcal{ELH}$ concepts. We prove the statement in two directions.

Assume $\mathcal{I}\models C\sqsubseteq D$ . By Lemma 53, we know $\mathcal{I}\models C\sqsubseteq D$ iff $\eta_{\mathcal{I}}\models C\sqsubseteq D$ , which means $\eta_{\mathcal{I}}(C)\subseteq\eta_{\mathcal{I}}(D)$ . By Proposition 5, this implies $\eta_{\mathcal{I}}^{*}(C)\subseteq\eta_{\mathcal{I}}^{*}(D)$ . Finally, by the definition of satisfaction, this is the case iff $\eta_{\mathcal{I}}^{*}\models C\sqsubseteq D$ . Now assume $\eta_{\mathcal{I}}^{*}\models C\sqsubseteq D$ . Then, by the semantics of geometric interpretation, $\eta_{\mathcal{I}}^{*}(C)\subseteq\eta_{\mathcal{I}}^{*}(D)$ . This means if $v\in\eta_{\mathcal{I}}^{*}(C)$ , then $v\in\eta_{\mathcal{I}}^{*}(D)$ , with $v=\sum_{i=1}^{n}\lambda_{i}v_{i}$ and $v_{1},\ldots,v_{n}\in\eta_{\mathcal{I}}(C)$ . So, assume $C^{\mathcal{I}}$ is non-empty. Then, there is $d\in C^{\mathcal{I}}$ , which, by Lemma 49 is the case iff $\mu(d)\in\eta_{\mathcal{I}}(C)$ . By the definition of convex hull, $\mu(d)\in\eta_{\mathcal{I}}^{*}(C)$ . By assumption, $\mu(d)\in\eta_{\mathcal{I}}^{*}(D)$ , and since $\mu(d)$ is binary, Corollary 7 gives us that $\mu(d)\in\eta_{\mathcal{I}}(D)$ . But again by Lemma 49, this is the case iff $d\in D^{\mathcal{I}}$ . Since $d$ was arbitrary, we have $\mathcal{I}\models C\sqsubseteq D$ . $\hfill\blacktriangleleft$

Lemma 71.

For all $r,s\in N_{R}$ , it is the case that $\mathcal{I}\models r\sqsubseteq s$ iff $\eta_{\mathcal{I}}^{*}\models r\sqsubseteq s$ .

Proof.

First, assume $\mathcal{I}\models r\sqsubseteq s$ . By Lemma 54, we know $\mathcal{I}\models r\sqsubseteq s$ iff $\eta_{\mathcal{I}}\models r\sqsubseteq s$ , which means $\eta_{\mathcal{I}}(r)\subseteq\eta_{\mathcal{I}}(s)$ . By Proposition 5, this implies $\eta_{\mathcal{I}}^{*}(r)\subseteq\eta_{\mathcal{I}}^{*}(s)$ , which, by the definition of satisfaction is the case iff $\eta_{\mathcal{I}}^{*}\models r\sqsubseteq s$ .

Assume $\eta_{\mathcal{I}}^{*}\models r\sqsubseteq s$ . Then, by the semantics of geometric interpretation, $\eta_{\mathcal{I}}^{*}(r)\subseteq\eta_{\mathcal{I}}^{*}(s)$ , which means if $v\in\eta_{\mathcal{I}}^{*}(r)$ , then $v\in\eta_{\mathcal{I}}^{*}(s)$ , where $v=\sum_{i=1}^{n}\lambda_{i}v_{i}$ for $v_{1},\ldots,v_{n}\in\eta_{\mathcal{I}}(r)$ . Assume $r^{\mathcal{I}}$ is non-empty. Then, there must be $(d,e)\in r^{\mathcal{I}}$ . We must now show $(d,e)\in s^{\mathcal{I}}$ is true. Since $(d,e)\in r^{\mathcal{I}}$ , by the definition of $\eta_{\mathcal{I}}$ , we have $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}(r)$ with both $\mu(d)$ and $\mu(e)$ being binary vectors. By the definition of convex hull, $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}^{*}(r)$ . Now, by assumption, $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}^{*}(s)$ , but since $\mu(d)\oplus\mu(e)$ is binary, by Corollary 7 we have that $\mu(d)\oplus\mu(e)\in\eta_{\mathcal{I}}(s)$ . By definition of $\eta_{\mathcal{I}}$ , we have that $\mu(d){[s,e]=1}$ . By definition of $\mu$ , for all $d^{\prime}$ such that $\mu(d^{\prime})=\mu(d)$ we have that $(d^{\prime},e)\in s^{\mathcal{I}}$ . In particular, this holds for $d^{\prime}=d$ . So $(d,e)\in s^{\mathcal{I}}$ . We have shown that if $(d,e)\in r^{\mathcal{I}}$ , then $(d,e)\in s^{\mathcal{I}}$ , which is the case iff $\mathcal{I}\models r\sqsubseteq s$ . $\hfill\blacktriangleleft$

See 31

Proof.

The result for IQs in normal form follows from Lemma 65; the one for concept inclusions follows from Lemmas 53 and 70; and the one for role inclusion follows from Lemma 54 and from Lemma 71. $\hfill\blacktriangleleft$

Lemma 72.

Let $\mathcal{O}$ be a normalized ${\cal ELH}$ ontology and let ${\mathcal{I}_{\mathcal{O}}}$ be the canonical model of $\mathcal{O}$ (Definition 26). The ${\mathsf{d}}$ -dimensional convex $\oplus$ -geometric interpretation of ${\mathcal{I}_{\mathcal{O}}}$ (Definition 29) is a strongly TBox faithful model of $\mathcal{O}$ . That is, $\mathcal{O}\models\tau$ iff $\eta^{\ast}_{\mathcal{I}_{\mathcal{O}}}\models\tau$ , where $\tau$ is either a concept inclusion in normal form or a role inclusion.

Proof.

Theorem 27 implies that if $\tau$ is an ${\cal ELH}$ CI in normal form or an ${\cal ELH}$ RI then $\mathcal{O}\models\tau$ iff ${\mathcal{I}_{\mathcal{O}}}\models\tau$ . From Lemma 70, we know $\eta_{\mathcal{I}}^{*}\models C\sqsubseteq D$ iff $\mathcal{I}\models C\sqsubseteq D$ , and by Lemma 71 we get that $\eta_{\mathcal{I}}^{*}\models r\sqsubseteq s$ iff $\mathcal{I}\models r\sqsubseteq s$ . This means that if $\tau$ is an ${\cal ELH}$ CI in normal form or an ${\cal ELH}$ RI then ${\mathcal{I}_{\mathcal{O}}}\models\tau$ iff $\eta^{\ast}_{\mathcal{I}_{\mathcal{O}}}\models\tau$ . $\hfill\blacktriangleleft$

See 32

Proof.

The theorem follows from Lemmas 69 and 72. $\hfill\blacktriangleleft$

A.4 Omitted proofs for Section 6

See 35

Proof.

Algorithm 1 has four main parts that are never executed in the same run, each corresponding to one of the normal forms that the input concept inclusion $\alpha$ can take.

$\alpha=A\sqsubseteq B$ :: In this case, the algorithm will execute lines 2–3. From assumption 1, line 3 spends time $O(1)$ and by assumption 3 this line is run $O({|\Delta^{\mathcal{I}}|})$ times. Hence, in this case, the algorithm consumes time $O({|\Delta^{\mathcal{I}}|})$ .
$\alpha=A_{1}\sqcap A_{2}\sqsubseteq B$ :: From assumption 3, the loop from lines 5–6 is executed $O({|\Delta^{\mathcal{I}}|})$ times. Each iteration consumes time $O(1)$ by assumption 1. Thus, Algorithm 1 runs in time $O({|\Delta^{\mathcal{I}}|})$ in this case.
$\alpha=A\sqsubseteq\exists r.B$ :: According to assumption 3, the nested loop from lines 8–11 uses time $O({{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ . The membership check in line 10 takes time $O({\mathsf{d}}\cdot{{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ , by assumption 4. Therefore, we get that Algorithm 1 requires time $O({\mathsf{d}}\cdot{\mathsf{n}}^{4})$ , where ${\mathsf{n}}={|\Delta^{\mathcal{I}}|}$ .
$\alpha=\exists r.A\sqsubseteq B$ :: Algorithm 1 will execute from lines 14–15 for CIs in this normal form. Each iteration of the for loop starting in line 14 consumes constant time according to assumption 1. Furthermore, the loop has $O({{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ iterations due to assumption 3. Hence, Algorithm 1 uses time $O({{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ for CIs in this normal form.

Therefore, Algorithm 1 consumes time $O({\mathsf{d}}\cdot{\mathsf{n}}^{4})$ . $\hfill\blacktriangleleft$

See 36

Proof.

We consider each the four forms that an ${\cal ELH}$ IQ in normal form $\alpha$ can assume separately. In each of them $a\in{\sf N_{I}}$ , $A,B\in{\sf N_{C}}$ , and $r\in{\sf N_{R}}$ .

$\alpha=A(a)$ :: Due to assumptions 1 and 2, line 2 uses time $O(1)$ .
$\alpha=(A\sqcap B)(a)$ :: As in the previous case, the assumption 1 and 2 imply that line 4 executes in time $O(1)$ .
$\alpha=(\exists r.A)(a)$ :: By assumption 3, line 7 is run $O({|\Delta^{\mathcal{I}}|})$ times, each iteration consuming time in $O({\mathsf{d}}\cdot{{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ (from assumptions 2 and 4). Therefore, Algorithm 2 spends time $O({\mathsf{d}}\cdot{\mathsf{n}}^{3})$ in such instance queries, where ${\mathsf{n}}={|\Delta^{\mathcal{I}}|}$ .
$\alpha=r(a,b)$ :: line 9 runs in time $O({\mathsf{d}}\cdot{{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ due to assumptions 2 and 4.

Therefore, Algorithm 2 consumes time $O({\mathsf{d}}\cdot{\mathsf{n}}^{3})$ . $\hfill\blacktriangleleft$

See 37

Proof.

There are $O({{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ iterations of the for loop starting in line 1 in a single run of Algorithm 3 as a consequence of the assumption 3. Additionally, each iteration consumes time $O({\mathsf{d}}\cdot{{|\Delta^{\mathcal{I}}|}\cdot{|\Delta^{\mathcal{I}}|}})$ by assumption 4. Therefore, Algorithm 3 runs in time $O({\mathsf{d}}\cdot{\mathsf{n}}^{4})$ , where ${\mathsf{n}}={|\Delta^{\mathcal{I}}|}$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Ralph Abboud, Ismail Ceylan, Thomas Lukasiewicz, and Tommaso Salvatori. BoxE: A box embedding model for knowledge base completion. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 9649–9661. Curran Associates, Inc., 2020. doi:10.5555/3495724.3496533.

[bib.bib2] [2] Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler. An Introduction to Description Logic. Cambridge University Press, USA, 1st edition, 2017. doi:10.1017/9781139025355.

[bib.bib3] [3] Antoine Bordes, Nicolas Usunier, Alberto Garcia-Duran, Jason Weston, and Oksana Yakhnenko. Translating embeddings for modeling multi-relational data. In C. J. Burges, L. Bottou, M. Welling, Z. Ghahramani, and K. Q. Weinberger, editors, Advances in Neural Information Processing Systems, volume 26. Curran Associates, Inc., 2013. doi:10.5555/2999792.2999923.

[bib.bib4] [4] Stefan Borgwardt and Veronika Thost. LTL over EL Axioms. Technische Universität Dresden, 2015. doi:10.25368/2022.213.

[bib.bib5] [5] Camille Bourgaux, Ricardo Guimarães, Raoul Koudijs, Victor Lacerda, and Ana Ozaki. Knowledge base embeddings: Semantics and theoretical properties. In Proceedings of the TwentyFirst International Conference on Principles of Knowledge Representation and Reasoning, pages 823–833, Hanoi, Vietnam, November 2024. International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/kr.2024/77.

[bib.bib6] [6] Camille Bourgaux, Ana Ozaki, and Jeff Z. Pan. Geometric models for (temporally) attributed description logics. In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, DL, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021. URL: https://ceur-ws.org/Vol-2954/paper-7.pdf.

[bib.bib7] [7] Jiaoyan Chen, Pan Hu, Ernesto Jimenez-Ruiz, Ole Magnus Holter, Denvar Antonyrajah, and Ian Horrocks. Owl2vec*: embedding of owl ontologies. Machine Learning, 110(7):1813–1845, July 2021. doi:10.1007/s10994-021-05997-6.

[bib.bib8] [8] Yuanfei Dai, Shiping Wang, Neal N. Xiong, and Wenzhong Guo. A Survey on Knowledge Graph Embedding: Approaches, Applications and Benchmarks. Electronics, 9(5):750, May 2020. doi:10.3390/electronics9050750.

[bib.bib9] [9] Claudia d’Amato, Nicola Flavio Quatraro, and Nicola Fanizzi. Injecting background knowledge into embedding models for predictive tasks on knowledge graphs. In Ruben Verborgh, Katja Hose, Heiko Paulheim, Pierre-Antoine Champin, Maria Maleshkova, Oscar Corcho, Petar Ristoski, and Mehwish Alam, editors, The Semantic Web, pages 441–457. Springer International Publishing, 2021. doi:10.1007/978-3-030-77385-4_26.

[bib.bib10] [10] Víctor Gutiérrez-Basulto and Steven Schockaert. From knowledge graph embedding to ontology embedding? an analysis of the compatibility between vector space representations and rules. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, KR, pages 379–388. AAAI Press, 2018. URL: https://aaai.org/ocs/index.php/KR/KR18/paper/view/18013, doi:10.4230/OASIcs.AIB.2022.3.

[bib.bib11] [11] Peter Gärdenfors. Conceptual Spaces: The Geometry of Thought. The MIT Press, March 2000. doi:10.7551/mitpress/2076.001.0001.

[bib.bib12] [12] Pascal Hitzler, Markus Krötzsch, and Sebastian Rudolph. Foundations of Semantic Web Technologies. Chapman & Hall/CRC, 2009.

[bib.bib13] [13] Anders Imenes, Ricardo Guimarães, and Ana Ozaki. Marrying query rewriting and knowledge graph embeddings. In RuleML+RR, pages 126–140. Springer-Verlag, 2023. doi:10.1007/978-3-031-45072-3_9.

[bib.bib14] [14] Mathias Jackermeier, Jiaoyan Chen, and Ian Horrocks. Dual box embeddings for the description logic el ${}^{\mbox{++}}$ . In Tat-Seng Chua, Chong-Wah Ngo, Ravi Kumar, Hady W. Lauw, and Roy Ka-Wei Lee, editors, Proceedings of the ACM on Web Conference, WWW, pages 2250–2258. ACM, 2024. doi:10.1145/3589334.3645648.

[bib.bib15] [15] Maxat Kulmanov, Wang Liu-Wei, Yuan Yan, and Robert Hoehndorf. EL embeddings: Geometric construction of models for the description logic EL++. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 6103–6109. ijcai.org, 2019. doi:10.24963/ijcai.2019/845.

[bib.bib16] [16] Victor Lacerda, Ana Ozaki, and Ricardo Guimarães. Faithel: Strongly tbox faithful knowledge base embeddings for $\mathcal{EL}$ . In Sabrina Kirrane, Mantas Šimkus, Ahmet Soylu, and Dumitru Roman, editors, Rules and Reasoning, pages 191–199, Cham, 2024. Springer Nature Switzerland. doi:10.1007/978-3-031-72407-7_14.

[bib.bib17] [17] Yankai Lin, Zhiyuan Liu, Maosong Sun, Yang Liu, and Xuan Zhu. Learning entity and relation embeddings for knowledge graph completion. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1), February 2015. doi:10.1609/aaai.v29i1.9491.

[bib.bib18] [18] Carsten Lutz and Frank Wolter. Deciding inseparability and conservative extensions in the description logic el. Journal of Symbolic Computation, 45(2):194–228, February 2010. doi:10.1016/j.jsc.2008.10.007.

[bib.bib19] [19] Sutapa Mondal, Sumit Bhatia, and Raghava Mutharaju. Emel++: Embeddings for EL++ description logic. In Andreas Martin, Knut Hinkelmann, Hans-Georg Fill, Aurona Gerber, Doug Lenat, Reinhard Stolle, and Frank van Harmelen, editors, AAAI-MAKE, volume 2846 of CEUR Workshop Proceedings. CEUR-WS.org, 2021. URL: https://ceur-ws.org/Vol-2846/paper19.pdf.

[bib.bib20] [20] Özgür Lütfü Özçep, Mena Leemhuis, and Diedrich Wolter. Cone semantics for logics with negation. In Christian Bessiere, editor, IJCAI, pages 1820–1826. ijcai.org, 2020. doi:10.24963/ijcai.2020/252.

[bib.bib21] [21] Aleksandar Pavlovic and Emanuel Sallinger. ExpressivE: A spatio-functional embedding for knowledge graph completion. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL: https://openreview.net/pdf?id=xkev3_np08z.

[bib.bib22] [22] Xi Peng, Zhenwei Tang, Maxat Kulmanov, Kexin Niu, and Robert Hoehndorf. Description logic EL++ embeddings with intersectional closure. CoRR, abs/2202.14018, 2022. arXiv:2202.14018, doi:10.48550/arXiv.2202.14018.

[bib.bib23] [23] Xi Peng, Zhenwei Tang, Maxat Kulmanov, Kexin Niu, and Robert Hoehndorf. Description logic EL++ embeddings with intersectional closure. CoRR, abs/2202.14018, 2022. arXiv:2202.14018.

[bib.bib24] [24] Théo Trouillon, Johannes Welbl, Sebastian Riedel, Éric Gaussier, and Guillaume Bouchard. Complex embeddings for simple link prediction. arXiv, June 2016. doi:10.48550/arXiv.1606.06357.

[bib.bib25] [25] Denny Vrandečić and Markus Krötzsch. Wikidata: A free collaborative knowledgebase. Commun. ACM, 57(10):78–85, September 2014. doi:10.1145/2629489.

[bib.bib26] [26] Bo Xiong, Nico Potyka, Trung-Kien Tran, Mojtaba Nayyeri, and Steffen Staab. Faithful embeddings for EL++ knowledge bases. In The Semantic Web – ISWC 2022, pages 22–38. Springer International Publishing, 2022. doi:10.1007/978-3-031-19433-7_2.

[bib.bib27] [27] Bishan Yang, Wen-tau Yih, Xiaodong He, Jianfeng Gao, and Li Deng. Embedding entities and relations for learning and inference in knowledge bases. arXiv, August 2015. arXiv:1412.6575.

[bib.bib28] [28] Frank Zenker and Peter Gärdenfors. Applications of Conceptual Spaces: The Case for Geometric Knowledge Representation, volume 359 of Synthese Library. Springer International Publishing, 2015. doi:10.1007/978-3-319-15021-5.

Strong Faithfulness for 𝓔⁢𝓛⁢𝓗 Ontology Embeddings

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Supplementary Material:

DOI:

Received:

Accepted:

Published:

Part Of:

Journal and Publisher:

1 Introduction

Contribution

2 Ontology Embeddings

3 Basic Notions

3.1 The Description Logic 𝓔⁢𝓛⁢𝓗

3.2 Geometric models

Example 1.

Definition 2 (Geometric Interpretation).

Definition 3.

Definition 4.

Proposition 5.

Theorem 6.

Corollary 7.

Definition 8 (Strong Faithfulness).

Example 9.

4 Strong Faithfulness

Definition 10.

▶ Remark 11.

Definition 12.

Theorem 13.

Definition 14.

Theorem 15.

Theorem 16.

Corollary 17.

Theorem 18.

Proof.

5 Strong Faithfulness on Convex Models

Definition 19.

Example 20.

Definition 21.

Example 22.

Example 23.

Proposition 24.

Theorem 25.

Definition 26.

Theorem 27.

Theorem 28.

Definition 29.

▶ Remark 30.

Theorem 31.

Theorem 32.

Corollary 33.

▶ Remark 34 (Number of parameters).

6 Model Checking on Geometric Models

Theorem 35.

Theorem 36.

Theorem 37.

7 Conclusion and discussion

References

Appendix A Appendix

A.1 Omitted proofs for Section 3

Proof.

Proof.

Proof.

A.2 Omitted proofs for Section 4

Lemma 38.

Proof.

Base case:

Inductive step:

Lemma 39.

Proof.

Lemma 40.

Proof.

Lemma 41.

Proof.

Lemma 42.

Proof.

Strong Faithfulness for $\mathcal{ELH}$ Ontology Embeddings

3.1 The Description Logic $\cal ELH$

$\blacktriangleright$ Remark 11.

$\blacktriangleright$ Remark 30.

$\blacktriangleright$ Remark 34 (Number of parameters).