Axioms

ONMA — axioms (mirror)

Ontological Sets and their Axioms

With the help of figure layers we will discuss in the following which laws result from the ontology structures. These laws can then be used to check the structural correctness of ontologies. Let P(M) be the powerset of a set M, C a class, T ⊆ C a subset of classes, and ∴C the set of classes of the class hierarchy of C. To compute the set of particulars of a class we define the function pof: C → P(E). To compute the set of particulars of a set of classes we define the function sop: P(C) → P(E) with:
{{definition:POF:Particulars OF a class:pof(C) := { y | (y, »pof, C) ∈ KG}.}}
{{definition:SOP:Set Of Particulars of classes:sop[T] := ∪ { pof(C) | C ∈ T}.}}
Then, we have as examples with ∴C3 = {C3, C4, C5, C6} ⊆ C as the set of particulars of a single class pof(C3) = {P3}, pof(C4) = {P4}, pof(C5) = {P5}, and pof(C6) = {P6, P7}. It follows that the SOPs of a class hierarchy of C3 is sop[∴C3] = sop[{C3, C4, C5, C6}] =  {P3} ∪ {P4} ∪ {P5} ∪ {P6, P7} = {P3, P4, P5, P6, P7}.
  Sets of Elements of Classes (SOE):
The set of particulars of a class differs from the Set Of Elements (SOE) of a class in that particulars can be fully instantiated (s. definition soa below) in the class. For each particular, however, there exists at least one class C ∈ C in which it can be fully instantiated. Then the function soe: C → P(E), which computes the set of elements of class C, can be defined as:
{{definition:SOE:Set Of Elements:soe(C) = ∪ {pof(X) | X ∈ ∴C}.}}

We denote the extension (ext) of a class C by extA(C) := C := soe(C). This leads to the axiom that a set of particulars of the class hierarchy of C is equivalent to the set of elements of the class C:

{{axiom:PECAx:Particulars-Elements-Correspondence:soe(C) = sop[∴C]. }}

Then we have for single classes sop(C4) = {P4} and sop(C6) = {P6, P7} and for their extensions C4 = soe(C4) = sop(∴C4) = {P4, P6, P7}, and C6 = soe(C6) = sop(∴C6) = {P6, P7}, and so on. Note, e.g., that P3 is an element of C1 but not a particular of C1. In general, all particulars of sublass C of a class D with D ≠ C and C ≤ D are elements of D but not particulars of D.

  Set of Attributes of Classes (SOA):
Let ∵c be the set of superclasses of c including c, and adtADT an atomic data type, and aA a data property. To compute the set of Data Property Definitions (DPD) of a class and its superclass hierarchy and associated set of attributes we define the functions sad: CP(A) and soa: CP(A) as follows:
{{definition:SAD:SAD = Set of Attribute Definitions:sad(C) := { a | (C, a, adt) ∈ KG ∨ (a, »hasDomain, C) ∈ KG}.}}
Then, the function soa() for computing the set of attributes in the hierarchy of superclasses of a class C is defined as:
{{definition:SOA:SOA = Set Of Class Attributes:soa(C) := ∪ {sad(X) | X ∈ ∵C}. }}

The Set Of Attributes (SOA) of a superclass hierarchy of C is also denoted as the intension of the class C with intA(C) := soa(C). It is important to realize that the instantiation of objects with data properties does not have to take on the full scope that would be possible based on the definition in the ontology schema. Therefore, we introduce the following definitions: Let x be a particular of the class C with (x, »pof, C) ∈ KG. If all attributes a ∈ intA(C) of an entity x are instantiated (have been assigned values), then we say “the entity x is fully instantiated”, otherwise, “the entity x is fully instantiable with attributes from intA(C)”.

So, the intension of a class is the set of attributes with which a particular of the class can be fully instantiated. That is, soa(C) is the set of attributes that have a Data Property Definition (DPD) in C or in the superclasses of C. Then we have, for example, sad(C1) = {A1}, sad(C2) = {A2}, sad(C3) = {A3}, ..., sad(C6) = {A6}. Furthermore, we have soa(C1) = {A1} ⊆ soa(C2) = {A1, A2}, soa(C3) = {A1, A3}, and soa(C3) ⊆ soa(C4) = {A1, A3, A4}, soa(C5), and soa(C4) ⊆ soa(C6) = {A1, A3, A4, A5, A6}. From this we already see that the smaller the intension of a class intA(C), the larger is its extension extA(C) = C. Then, e.g., a particular P2 of C2 is fully instantiable with the set of attributes soa(C2) = {A1, A2}. This is equivalent to (P2, »pof, C2) ∈ KG. However, neither the attribute A1 nor A2 need to have a value assigned to P2.

In the following, in analogy to data properties we give set definitions for object properties. The set of outgoing object properties of a class C is defined as the set of OPs where C is the domain OP. This set is also denoted as the OP intension of the class C with intR(C) := sdp(C). We define sdp: CP(R) as:

{{definition:SDP:SDP = Set of Domain OPs:sdp(C) := { ◊op | (C, ◊op, D) ∈ KG ∨ (◊op, »hasDomain, C) ∈ KG}.}}

In analogy to a class hierarchy the hierarchy of Object Properties (OP) is defined as (R , ≤) and has the set of OPs ∴R := {r ∈ R | r ≤ R} with x ≤ y ⇔ x, y ∈ R: (x, »subOpOf, y) ∈ KG. Then, for the set of object property particulars EEE X E of an OP ◊R we define a function soopp: R → P(EE) with:

{{definition:SOOPP:Set Of OP Particulars:soopp(◊R) := {(x, y) | (x, »R , y) ∈ KG }. }}
To compute the set of elements of an OP hierarchy, we define the function soope: R → P(EE). We also denote R := extR(R) := soope(R) as the extension of R.
{{definition:SOOPE:Set Of Object Property Elements:soope(R) := ∪ {soopp(r) | r ∈ ∴R}. }}

The set of pairs (x, y) of arbitrary OPs where C is the domain class is denoted as the OP extension of C with extR(C):= soopi(C). With soopi: CP(EE) we define:

{{definition:SOOPI:Set Of Object Property Instances:soopi(C) := {(x, y) | (x, »r, y) ∈ KG ∧ x ∈ pof(C) ∧ ◊r ∈ sdp(C)}. }}
Figure psop1 shows a small example from the domain of cars and motors. To the left of the schema layer we see a subclass hierarchy of cars which is based on their type of motorization, to the right the corresponding subclass hierarchy of motors. Both subhierarchies contain with HybridCar and HybridMotor a class with multiple inheritance. The corresponding pairs of classes are connected by the OP definitions (Car, ◊hasMotor, Motor), (CombCar, ◊hasCombMotor, CombMotor), (ElectricCar, ◊hasElectricMotor, ElectricMotor), and also (HybridCar, ◊hasHybridMotor, HybridMotor). Each class has a particular which is connected by »pof to its class. For the class extensions we have:
  • HybridCar = {MP}, CombCar = {TL, MP}, ElectricCar = {MT, MP}, Car = {HP, TL, MT, MP},
  • HybridMotor = {MMP}, CombMotor = {MTL, MMP}, ElectricMotor = {MTT, MMP}, Motor = {MHP, MTL, MTT, MMP}.
The set of Object Property Instances (OPI) is formed by the triples (HP, »hasMotor, MHP), (TL, »hasCombMotor, MTL), (MT, »hasElectricMotor, MTT), and (MP, »hasHybridMotor, MMP). Then, soopp (◊hasMotor) = { (HP, MHP) }, soopp (◊hasCombMotor) = { (TL, MTL) }, soopp (◊hasElectricMotor ) = { (MT, MTT) }, and soopp (◊hasHybridMotor ) = { (MP, MMP) }. From this we can derive the extensions of the OPs as
  • ◊hasHybridMotor = {(MP, MMP)}
  • ◊hasElectricMotor = {(MT, MTT), (MP, MMP)}
  • ◊hasCombMotor = {(TL, MTL), (MP, MMP)}
  • ◊hasMotor = {(MP, MMP), (MT, MTT), (TL, MTL), (MP, MMP)}
Then, for the hierarchy and the extensions of the OPs we have
  • ◊hasHybridMotor ≤ ◊hasElectricMotor,
  • ◊hasHybridMotor ≤ ◊hasCombMotor,
  • ◊hasCombMotor ≤ ◊hasMotor,
  • ◊hasElectricMotor ≤ ◊hasMotor
  • ◊hasHybridMotor◊hasElectricMotor,
  • ◊hasHybridMotor◊hasCombMotor,
  • ◊hasCombMotor◊hasMotor,
  • ◊hasElectricMotor◊hasMotor

For example, for electric cars we have (ElectricCar, ◊hasElectricMotor, ElectricMotor) ∈ KG ∧ (MT, »hasElectricMotor, MTT) ∈ KG → MT ∈ pof(ElectricCar) ∧ MTT ∈ pof(ElectricMotor) ⇔ (MT, »pof, ElectricCar) ∈ KG ∧ (MTT, »pof, ElectricMotor) ∈ KG or in general with (C, ◊R, D) ∈ KG ∧ (P, »R, Q) ∈ KG → P ∈ pof(C) ∧ Q ∈ pof(D) ⇔ (P, »pof, C) ∈ KG ∧ (Q, »pof, D) ∈ KG.

pdf:psop1:1.0
Object Property Hierarchy for Cars and Motors

Class Subsumption Axiom

From the above examples we see soe(C4) ⊆ soe(C3) ⇔ (C4, ≤, C3) ⇔ int(C3) = soa(C3) ⊆ int(C4) = soa(C4). This is consistent with the axioms in Formal Concept Analysis (FCA) as described in [Pris1998], because the set E corresponds to formal objects (Gegenstände) and A corresponds to formal attributes (Merkmale). For I ⊆ E x A, the relation ≤is called formal conceptual ordering on the set of all formal concepts B(E, A, I). So, in general we can define an extended class subsumption axiom (CSAx) as:
{{axiom:CSAx:CSAx = Class Subsumption Axiom: soe(C) ⊆ soe(D) ⇔ C ≤ D ⇔ sop[∴C] ⊆ sop[∴D] ⇔ soa(D) ⊆ soa(C). }}
As pointed out in [LuZe2021], we can consider an ontology to be correct with respect to the structure of its classes, attributes, and particulars, if elements from C, A, and E constitute a formal concept. As an important result we find that only from the set of attributes A of particulars E we can infer its class hierarchy structure C∴ = (C, ≤). Therefore, it is possible with FCA methods to automatically identify class candidates based on simple cross-tables, where it is only necessary to mark with an X those objects e ∈ E which have attributes a ∈ A.

The complete class hierarchy C of an ontology O can usually consist of several sub-hierarchies ∴CiC which model different areas of the application domain, e.g., ∴C1 = ∴Person, ∴C2 = ∴Car, ∴C3 = ∴Motor etc. An attribute A can only be defined once in C. The reason for this is that otherwise the subsumption axiom Ax CSAx would be violated. I.e., if the attribute A occurs more than once in CxC and Cy C, then it must be moved to the smallest / lowest common superclass Cz of Cx and Cy, so that both Cz ∈ ∵Cx and Cz ∈ ∵Cy hold.

Relationship Type Subsumption Axiom

According to Lübbert and Zeh [LuZe2021], page 8 ff, the subsumption principle can now also be used to automatically detect hierarchies of Relationship Types (RT). We define the subsumption axiom for object properties based on the insight that an object property ◊R is a direct or indirect subobject property of the object property ◊S if its elements are a subset of the elements of its superobject property:

{{axiom:RTSAx:RTSAx = Relationship Type Subsumption Axiom: soope(◊R) ⊆ soope(◊S) ⇔ ◊R◊S ⇔ ◊R ≤ ◊S. }}
Now let us consider the consequences that follow from OP ordering relations. Let ◊T be an object property and ◊R, ◊S ∈ ∴◊T with ◊R ≤ ◊S and ◊R ≠ ◊S, and C, D ∈ C, and C1, C2 ∈ ∴C, D1, D2 ∈ ∴D, (C1, ◊R, D1) ∈ KG, and (C2, ◊S, D2) ∈ KG. Then, with p ∈ pof(C1), q ∈ pof(D1), and (p, q) ∈ ◊R follows (p, q) ∈ ◊S. This also means with soe(C2) = C2  and soe(D2) = D2 that p ∈ C2 ∧ q ∈ D2 and this is exactly the case if C1 ≤ C2 ∧ D1 ≤ D2 where also holds C1C2D1D2. This is also true for the cases where C1 = C2 and D1 = D2. This means that pairs of particulars that make up the extension of an OP automatically force the arrangement in the respective domain and range class of the OP. For example, for the OPs hasMotor, hasElectricMotor, hasCombMotor and hasHybridMotor each have a specific motor type as the range entity of the pair (x, y). Since the motor types are arranged in an inheritance hierarchy ∴Motor, the domain entities are also automatically arranged in an isomorphic inheritance hierarchy. This leads to the following consideration: Even if the class Car has no subclass, the ordering relation for the subclass hierarchy ∴Car can be inferred from the OP hierarchy of ◊hasMotor, e.g., in (x, »hasElectricMotor, y) the object y must be a particular of ElectricMotor, and from this it can be inferred that x must be an ElectricCar. This leads to the definition of properly suspended relationship types:

{{definition:PSRT:Properly Suspended RT: Be ◊R ≤ ◊S. ◊R is properly suspended under ◊S if: ((C1 ≤ C2) ∧ (D1 ≤ D2)) ⇔ (( C1C2) ∧ (D1D2)) .}}

Then we claim a subsumption theorem for relationship hierarchies in analogy to axiom PECAx. The statement is: For a pair of object properties where one OP is a subobject property of the other (◊R ≤ ◊S), the domain and range classes involved must be superclasses and subclasses of each other, respectively.

{{theorem:RTSTh:RTSTh = RT Subsumption Theorem: ◊R ≤ ◊S → (C1 ≤ C2) ∧ (D1 ≤ D2). }}

Proof of RTSTh: Suppose that C1 ≤ C2 or D1 ≤ D2 does not hold. Then we would have C1 > C2 or D1 > D2, and C1C2 or D1D2. This would imply that the more general class has fewer elements than one of its subclasses, e.g., there are more ElectricMotors than Motors or more ElectricCars than Cars. This leads to a contradiction. □

Applying these principles, we can now use Formal Concept Analysis (FCA) to extend the lattices of classes to lattices of their object properties. As formal objects we use the set of pairs EE= {(x, y) | x, y ∈ E} and as formal attributes the set R. Then, e.g., from object property instances such as (x, »hasCombMotor, y), we find order relations of the form »hasHybridMotor ≤ »hasCombMotor, »hasElectricMotor ≤ »hasMotor. Analogous to the class hierarchy, I ⊆ EE x R and the relation ≤ is the formal concept ordering and the set of all formal relationship type concepts is BR(EE, R, I).

In the example (^Car, ◊hasMotor, ^Motor), the class ^Car can be understood as an aggregator and ^Motor as an aggregatee. In the example (^Artist, ◊isCreatorOf, ^Artifact) the situation is reversed (see lattices of relationship types in [LuZe2021], page 8 ff). Here ◊isCreatorOf can be understood as an OP that classifies ^Artist in relation to the type of the produced ^Artifact, e.g. with ◊isSculptorOf ≤ ◊isCreatorOf, ◊isOilPainterOf ≤ ◊isPainterOf ≤ ◊isCreatorOf, and ◊isCreatorOf = ◊hasCreator-1. That is why in our interpretation, the general OPs ◊has and ◊is from figure o4toptl2 are considered dual / orthogonal to each other. All OPs that are derived from ◊has can be attributed to aggregation, all OPs that are derived from ◊is can be attributed to classification / generalization.

Class Identity Axiom

As an extended axiom, we define that a class C is identical to another class D if both their attribute and relationship type intensions, as well as their element and object property extensions are identical. Be C, D ∈ C.

{{axiom:CIdAx:CIdAx = Class Identity Axiom: (intA(C) = intA(D)) ∧ (intR(C) = intR(D)) ∧ (C = D) ∧ (extR(C) = extR(D)) → C = D.}}

Extension: deriver.app

Related: Preliminaries — Definitions (O4Top & Instantiation on the same page); Theory — Axioms. Deriver documentation.

Source: taoke.de — ONMA — Axioms.