Axioms
ONMA — axioms (mirror)
Ontological Sets and their Axioms
Sets of Elements of Classes (SOE):
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:
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):
∵c be the set of superclasses of c including c, and adt ∈ ADT an atomic data type, and a ∈ A 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: C → P(A) and soa: C → P(A) as follows: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: C → P(R) as:
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 EE = E X E of an OP ◊R we define a function soopp: R → P(EE) with:
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: C → P(EE) we define:
- 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}.
- ◊hasHybridMotor = {(MP, MMP)}
- ◊hasElectricMotor = {(MT, MTT), (MP, MMP)}
- ◊hasCombMotor = {(TL, MTL), (MP, MMP)}
- ◊hasMotor = {(MP, MMP), (MT, MTT), (TL, MTL), (MP, MMP)}
- ◊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.
Class Subsumption Axiom
The complete class hierarchy C of an ontology O can usually consist of several sub-hierarchies ∴Ci ⊆ C 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 Cx ∈ C 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:
{{definition:PSRT:Properly Suspended RT: Be ◊R ≤◊ ◊S. ◊R is properly suspended under ◊S if: ((C1 ≤∧ C2) ∧ (D1 ≤∧ D2)) ⇔ (( C1 ⊆ C2) ∧ (D1 ⊆ D2)) .}}
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.
Proof of RTSTh: Suppose that C1 ≤∧ C2 or D1 ≤∧ D2 does not hold. Then we would have C1 >∧ C2 or D1 >∧ D2, and C1 ⊃ C2 or D1 ⊃ D2. 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
Extension: deriver.app
Related: Preliminaries — Definitions (O4Top & Instantiation on the same page); Theory — Axioms. Deriver documentation.
Source: taoke.de — ONMA — Axioms.
