# Introduction WL 2 Web Ontology Language (OWL 2) [1] is a language of knowledge representation used for defining ontologies. The ontologies which satisfy syntactic conditions listed in the specification in Section 3 of [2] are called OWL 2 DL ontologies and have their semantics expressed in SROIQ description logic [1]. SROIQ was designed to provide additions to OWL-DL to guarantee decidability in reasoning [3,4]. The domain ontologies are expected to provide a knowledge base about specific application area. Therefore they should be consistent. An ontology consistency check [5] is one of the reasoning problems that can be answered with the use of inference engines. In our work, we would like to take advantage of and reuse the existing OWL 2 DL domain ontologies. We assume that the selected OWL 2 DL domain ontology is syntactically correct, consistent and adequately describes the notions from the needed domain. One can successfully conduct reasoning over the ontology with the use of one of the reasoning engines available. However, it is not obvious or conclusive how to effectively process other useful operations on ontologies, for example how to compare two or more ontologies. The problem of comparing two ontologies with the agreed vocabulary was faced in [6] in a method of semantic validation of UML class diagrams. In [6], in the beginning, the UML class diagram is transformed into an ontology expressed in OWL 2. Next, the two ontologies-the domain ontology and the ontological representation of the UML diagram-need to be compared against each other. The question arises: how to correctly and automatically find out whether one ontology is compliant or contradictory concerning another one ? For the purpose of answering the question, we introduce such a form of normalization that allows for unifying the structure of axioms in the ontologies so that it is possible to automatically compare them. The method of normalization of ontologies and the method of semantic validation of UML class diagrams has been implemented in the prototype tool [8]. This paper presents the details of conducting the transformation of OWL 2 ontology to its normalized form. The important fact is that the presented transformations only change the structure but do not affect the semantics of axioms or expressions in the OWL 2 ontology. We propose the following groups of transformations of OWL 2 constructs: Group I. Extraction of declarations of entities: A declaration in OWL 2 associates an Entity with its type. If a declaration axiom for the selected Entity is missing from the ontology, it can be retrieved based on the usage of the Entity. In OWL 2, the declaration axiom can be specified for all types of entities: Class, Datatype, ObjectProperty, DataProperty, AnnotationProperty and NamedIndividual. Group II. Removal of duplicates in data ranges, expressions, and axioms: Following [2], sets written in one of the exchange syntaxes (e.g., XML or RDF/XML) may contain duplicates. Therefore, duplicates (if applicable) are eliminated from axioms (e.g. EquivalentClasses), data ranges (e.g. DataUnionOf) and expressions (e.g. DataUnionOf). Group III. Restructuration of data ranges and expressions: The proposed restructurations are intended (1) to flatten the nested structures of the data ranges and expressions, (2) to eliminate the weakest cardinality restrictions included in the data ranges or expressions, and (3) to refactor the data ranges and expressions which are connected with union, intersection and complement constructors, based on the rules of the De Morgan's laws. Group IV. Removal of syntactic sugar in axioms: OWL 2 offers the so-called syntactic sugar [4]. The syntactic sugar makes some axioms easier to write and read for humans (e.g., DisjointUnion axiom) but does not lend itself so easily to processing conducted by tools. Due to this fact, the removal of syntactic sugar allows e.g., easier comparison of axioms expressing the same semantics but written with a different syntax. Group V. Restructuration of axioms: Most of OWL 2 axioms which contain several class expressions can be restructured into several axioms containing only two class expressions each, e.g., DisjointClasses and EquivalentClasses axioms. This is only worth to be applied for axioms whose order of internal expressions is not important. Group VI. Removal of duplicated axioms: A correctly specified OWL 2 ontology cannot contain two identical axioms (see Section 3). However, duplicated axioms may appear as a result of applying transformations from groups IV and V. Therefore, the last step of the normalization algorithm is to remove all duplicate axioms from the output ontology. We define ontology normalization as a process of transforming the input ontology into the ontology in its refactored form. In Section 4, we presented replacing and replaced OWL 2 constructs used in the process of normalizing OWL 2 DL ontologies. The details of the ontology normalization algorithm are presented in Section 5. The process consists of four phases, which are executed in the following order in the algorithm: 1. Extraction of declarations (group I). # Refactorization of data ranges and expressions through applying transformations from group II. # Restructuration of expressions and data ranges through applying transformations from group III. 4. Refactorization of axioms through applying transformations from groups II, IV, V and VI. We consider the output ontology (obtained as a result of conducting the algorithm) as normalized. Because all transformations (of the replaced OWL 2 constructs to the replacing OWL 2 constructs) preserve semantics, the semantics of the normalized ontology is the same as the semantics of the input ontology. In this paper, OWL 2 constructs are written with the use of functional-style syntax [2]. Additionally, the following convention is used: II. ? C ? # Related Work According to our investigation, a similar concept of normalization of OWL 2 ontologies has not yet been proposed. In this paper, the normalization is aimed at unifying the structure of axioms in the ontologies allowing for automatic processing of the ontologies. A different purpose (as well as a different kind of) ontology normalization has been proposed in [9], where ontology normalization was suggested to be a pre-processing step that aligns structural metrics with intended semantic measures. Additionally, in [10] and [11], normalization has been proposed as an aspect of ontology design that provides support for ontology reuse, maintainability, and evolution. In [10] and [11] the criteria for normalization are focused on engineering issues that make ontologies modular and understandable for knowledge engineers. # III. OWL 2 Ontology as a Set of Axioms The structural specification of OWL 2 [2] is defined with the use of Unified Modeling Language (UML) [7], and the notation is compatible with Meta-Object Facility (MOF) [12]. OWL 2 ontologies consist of entities (classes, datatypes, object properties, data properties, annotation properties and named individuals), expressions (class expressions, data and object property expressions) and axioms (e.g., subclass axioms). The main component of OWL 2 ontologies is axioms (see fig. 1) which specify what is true in a specific domain. The expressions are used to represent complex notions in the described domain. Textually, expressions can be seen as components of axioms, for example, two or more class expressions are needed to specify DisjointClasses axiom (see fig. 2). Finally, entities constitute the vocabulary of an ontology. Because the association end named axioms (see fig. 1) is specified with the use of UML Multiplicity Element and a Set collection type (is Ordered=false and is Unique=true), a correct OWL 2 ontology cannot contain two axioms that are textually equivalent. In the normalization method, it is assured through applying the transformations from group VI. Nevertheless, the ontology may have axioms which contain the same information. For example, it may include the following two axioms: DisjointUnion (:Child :Boy :Girl ) and DisjointClasses(:Boy: Girl). The semantics of DisjointUnion [2] states that Child class is a disjoint union of Boy and Girl class expressions which are pairwise disjoint. Therefore, the additional information specified by DisjointClasses can be seen as redundant and will be refactored with the proposed transformation rules (here from groups II and IV). The structural specification of OWL 2 [2] defines an abstract class Axiom (see fig. 3). The abstract class Axiom is specialized by the following classes: ClassAxiom (abstract), ObjectPropertyAxiom (abstract), DataPropertyAxiom (abstract), Declaration, Datatype Definition (abstract), HasKey, Assertion (abstract) and AnnotationAxiom (abstract). # Fig. 3: The axioms of OWL 2 [2]and the tables which specify the proposed replacement rules. AnnotationAxiom [2] axioms are mainly used to improve readability for humans. The axioms do not affect the semantics [2]. Therefore, they are not further restructured in this paper. Declaration [2] axioms specify that entities are part of the vocabulary in ontology and are of a specific type, e.g., class, datatype, etc. OWL 2 DL ontology must explicitly declare all datatypes that occur in datatype definition, although in general, it is advisable to declare all entities for verification of the correctness of the usage of the entity based on its type. In the normalization method, if a declaration axiom is missing from the ontology, it is automatically retrieved based on the entity usage (transformation from the group I). This is applied toall types of entities but AnnotationProperty, because AnnotationProperty is only used to provide annotation and has no effect on the semantics. Datatype Definition [2] axiom defines a new datatype as being semantically equivalent to a unary data range. The Datatype Definition axiom is defined in the form that does not need to be restructured. Nonetheless, the data ranges included in other axioms or expressions may require refactoring (transformation from group III). The replacement rules for data ranges are presented in Table 5. HasKey [2] axiom states that each named instance of the specified class expression is uniquely identified by the specified object property and/or data property expressions. It is useful in querying about individuals which are uniquely identified. The HasKey axiom itself is defined in the form that does not need to be restructured, but the class expression and object property expressions included in the axiom are restructured by the transformations presented in Tables 6 and 7 (transformation from group III). To summarize, Section 4 presents replacement rules for Class Axioms in Table 1, for Object Property Axioms in Table 2, for Data Property Axioms in Table 3 and Assertion axioms in Table 4, Table 5 presents replacement rules for data ranges, Table 6 -for class expressions and Table 7 for object property expressions. Each row in Tables 1-7 contains the number of the transformation group (by Groups I-VI defined in Introduction). Additionally, all the transformations from Group III are marked with the subnumber (1)-( 3) which defines a concrete refactorization within the group. # IV. OWL 2 Construct Replacements Each replaced OWL 2 construct is semantically equivalent to the defined replacing construct(s). Most of the proposed transformations are our original proposals, but some of them come from the OWL 2 specification [2]. The specification defines the so-called syntactic sugar for selected axioms in more detail. This is for ease of writing of some popular patterns for humans. It is cited, where applicable, separately in each table. # a) Class expression axioms OWL 2 class expression axioms define the relationships between class expressions. The abstract class ClassAxiom is specified by the following concrete classes: SubClassOf, EquivalentClasses, DisjointClasses and DisjointUnion. In Table 1, transformations of IDs: 3, 6 and 8 are defined in [2], the other transformations are proposed by us. The replacing axioms in ID 6 are semantically equivalent. 3, transformations of IDs: 3 and 6-8 are defined in [2], the remaining transformations are proposed by us. DifferentIndividuals( a i a j ) and i,j ? {1,N} and i ? j and N ? 2 e) Data ranges OWL 2 data ranges [2] are used in restrictions on data properties. The abstract class DataRange is specified by the following concrete classes: DataComplementOf, DataUnionOf, DataOneOf, Datatype, DatatypeRestriction and DataIntersectionOf. In Table 5, all transformations are our own proposals. The reason is that in both class expressions the data range DR arity MUST be N (N ? 2). However, the current version of OWL 2 specification [2] does not provide any constructor, which may be used to define data ranges of arity more than one (see Section 7 of [2]). If a future version of the specification provides such a constructor, one can consider removal of duplicates and further restructuration of the mentioned class expressions. 7, the transformation is our proposal. # Table 7: The replaced and replacing object property expressions. # ID Group Replaced object property expression Replacing object property expression 1 III(3) ObjectInverse of( ObjectInverse Of ( OP ) ) OP # V. Ontology Normalization Algorithm The following is an outline of the algorithm which transforms the syntactically correct and consistent OWL 2 DL ontology selected by the user ? denoted by OWL ONT ? into the normalized ontology. The OWL ONT ' and OWL ONT '' are intermediate ontologies required to process the input ontology into the output ontology. In the beginning, both OWL ONT ' and OWL ONT '' are empty. On completion of the algorithm, the OWL ONT '' represents the normalized ontology. # Global Journal of Computer Science and Technology Volume XVIII Issue II Version I # Input: Syntactically correct and consistent OWL 2 DL ontology Output: Normalized OWL 2 DL ontology BEGIN 1. Take the first axiom from OWL ONT . 2. Take the first entity from the selected axiom. 3. If the entity is declared, add the declaration axiom to OWL ONT '.If the entity is not declared, extract the declaration axiom for the entity based on its usage and add the new declaration axiom to OWL ONT '. 4. Take the next entity from the selected axiom. 5. Repeat steps 3-4 until no more entities in the selected axiom are available. 6. Apply to the selected axiom allapplicable replacement rules defined in Tables 5-7, receiving a modified axiom. 7. Add the modified axiom to OWL ONT '. 8. Take the next axiom from OWL ONT . 9. Repeat steps 2-8 until no more axioms in OWL ONT are available. 10. Take the first axiom from OWL ONT '. 11. Apply to the axiom allapplicable replacement rules defined in Tables 1-4. 12. If transformations result in only one axiom, add the axiom to OWL ONT ''. Otherwise, if as a result of transformations the axiom splits into two or more axioms, repeat step 11 for each split axiom independently. 13. Take the next axiom from OWL ONT '. 14. Repeat steps 11-13 until no more axioms in OWL ONT ' are available. 15. Eliminate any of the duplicated axioms from OWL ONT '' ontology. 16. Return the OWL ONT '' as a normalized ontology. END Comments to the algorithm: 1. OWL 2 ontologies are built of axioms which may contain some expressions. Data ranges are contained in two axioms: DatatypeDefinition and DataPropertyRange, as well as in some expressions, e.g.,DataAllValuesFrom, DataMinCardinality, etc. Therefore, to perform fewer iterations of the normalization algorithm, first, we conduct all the transformations of the data ranges in axioms and expressions, as well as the expressions in axioms, and later on of the axioms themselves. 2. If the input ontology does not contain any duplicated axioms, the resulting ontology will contain at least the same number of axioms as the input ontology. 3. The order of the conducted transformations is not important because the resulting ontology will always be semantically equivalent. However, depending on the selected order, the resulting ontology may have a different textual form. The possible textual differences in the output ontology include: (1) the order of axioms and (2) the order of expressions in axioms (only if the order of expressions in the selected axiom is not important). 4. The resulting ontology may contain fewer kinds of axioms and expressions. In particular, the ontology will not contain the below-mentioned list of axioms and expressions because they are refactored and reduced in accordance with the presented transformations: ? Class axioms: EquivalentClasses, DisjointClasses, DisjointUnion, ? Object property axioms: EquivalentObjectProperties, InverseObjectProperties, ObjectPropertyDomain, ObjectPropertyRange, InverseFunctionalObject Property, FunctionalObjectProperty, ReflexiveObject Property, IrreflexiveObjectProperty, SymmetricObject Property,TransitiveObjectProperty, ? Data property axioms: EquivalentDataProperties, DataPropertyDomain, DataPropertyRange, Functional DataProperty, ? Class expressions: ObjectSomeValuesFrom, Object AllValuesFrom, ObjectHasValue, ObjectExact Cardinality, DataSomeValuesFrom, DataAllValues From, DataHasValue, DataExactCardinality. 5. The method of normalization and the defined transformations are unidirectional, which means that it is not possible to retrieve the original ontology from the normalized ontology. # VI. Example of Single Normalization The example presents transformations conducted with the use of the normalization algorithm. The following is an input ontology, which contains one axiom: EquivalentClasses(:FourLeafClover: FourLeafClover ObjectIntersectionOf( ObjectMinCardinality(3: hasLeaf:Leaf ) ObjectMaxCardinality( 7 :hasLeaf :Leaf ) ObjectExactCardinality( 4 :hasLeaf :Leaf ) ) ) Steps 1-5 of the algorithm extract declarations of entities: Declaration( Class ( :FourLeafClover ) ) (1) Declaration( Class ( :Leaf ) ) (2) Declaration( ObjectProperty (:hasLeaf ) ) Steps 6-9 of the algorithm result in the following transformations: Rule 19 from # The interpretation of ObjectUnionOf( CE 1 ... CE N ) is (14) [13]: (???? 17) and (18) are equal, which had to be proved. # VIII. Conclusions The paper introduces the concept of ontology normalization as a process of transforming the input OWL 2 ontology into the ontology in its refactored form. The process is defined through a group of OWL 2 construct replacements. Because all individual replacing constructs preserve the semantics of the replaced constructs, the resulting ontology does not change the semantics of the original ontology. Thanks to the presented approach, users obtain the possibility to automate the processing of ontologies because the normalized ontologies have the structure of axioms unified. However, the normalized ontology has reduced readability from the point of view of human readers, which is caused especially by the transformations from the group IV, which remove the syntactic sugar from the ontology. The presented normalization algorithm is implemented in a prototype tool [8] which additionally allows for comparing two ontologies with the agreed vocabulary. More specifically, the tool states whether or not two ontologies are compliant or contradictory by the method outlined in [6]. ![indicates a class, ? CE (possibly with an index) ? indicates a class expression, ? OP ? indicates an object property, ? OPE (possibly with an index) ? indicates an object property expression, ? DP ? indicates a data property, ? DPE (possibly with an index) ? indicates a data property expression, ? DR ? indicates a data range, ? a ? indicates an individual, ? lt ? indicates a literal, ? ? = ? -means the textual identity of ? and ? OWL 2 constructs.](image-2.png "") 1![Fig.1: A relation between OWL 2 ontology and axioms (extract from Figure 1 of OWL 2 specification [2]).](image-3.png "Fig. 1 :") 2![Fig.2: A relation between the selected class axiom, relevant expressions and entities (by OWL 2 specification [2]).](image-4.png "Fig. 2 :") 1ID GroupReplaced axiomReplacing axiom(s)1II2V3IV4II5V6IV7II8IVb) Object property axiomsOWL 2 object property axioms define therelationships between property expressions. Theabstract class ObjectPropertyAxiom is specified by thefollowing concrete classes: SubObjectPropertyOf,EquivalentObjectProperties, Disjoint Object Properties,InverseObjectProperties, ObjectPropertyDomain, ObjectPropertyRange,ReflexiveObjectProperty,IrreflexiveObjectProperty,FunctionalObjectProperty,InverseFunctionalObjectProperty,SymmetricObjectProperty,AsymmetricObjectProperty and TransitiveObjectProperty. In 2The Method of Normalizing OWL 2 DL OntologiesYear 20184Volume XVIII Issue II Version I ( ) CEquivalentClasses( CE 1 CE 2 ) DisjointClasses( CE 1 ... CE i ... CE j ... CE N )SubClassOf( CE 1 CE 2 ) SubClassOf( CE 2 CE 1 ) DisjointClasses( CE 1 ... CE i ... CE N )Global Journal of Computer Science and Technologyand 1 ? i ? j ? N and N ? 3 and CE i = CE j DisjointClasses( CE 1 ... CE N ) and N ? 2 DisjointClasses( CE 1 CE 2 ) DisjointUnion( C CE 1 ... CE i ... CE j ... CE N ) and 1 ? i ? j ? N and N ? 3 and CE i = CE j DisjointUnion( C CE 1 ... CE N ) and N ? 2and 1 ? i ? N and N ? 2 DisjointClasses( CE i CE j ) and i,j ? {1,N} and i ? j and N ? 2 SubClassOf (CE 1 ObjectComplementOf( CE 2 ) ) SubClassOf (CE 2 ObjectComplementOf( CE 1 ) ) DisjointUnion( C CE 1 ... CE i ... CE N ) and 1 ? i ? N and N ? 2 EquivalentClasses( C ObjectUnionOf ( CE 1 ... CE N ) ) DisjointClasses( CE 1 ... CE N ) and N ? 2© 2018 Global Journals 1EquivalentClasses( CE 1 ... CE i ... CE N ) and 1 ? i ? N and N ? 2 EquivalentClasses ( CE i CE j ) and i,j ? {1,N} and i ? j and N ? 2 2ID GroupReplaced axiomReplacing axiom(s)IIVIVIIVIVIVIVIV10IV11IV12IV13IV14IVc) Data property axiomsEquivalentDataProperties, DisjointDataProperties, DataOWL 2 data property axioms define thePropertyDomain, DataPropertyRange, and Functionalrelationships between property expressions. TheDataProperty.In Tableabstract class DataProperty Axiom is specified by thefollowing concrete classes: SubDataProperty Of, 3The Method of Normalizing OWL 2 DL OntologiesEquivalentObjectProperties( OPE 1 ... OPE i ...OPE N )and 1 ? i ? N and N ? 2EquivalentObjectProperties( OPE i OPE j )and i,j ? {1,N} and i ? j and N ? 2EquivalentObjectProperties( OPE 1 OPE 2 )SubObjectPropertyOf( OPE 1 OPE 2 ) SubObjectPropertyOf( OPE 2 OPE 1 )DisjointObjectProperties( OPE 1 ... OPE i ... OPE jDisjointObjectProperties( OPE 1 ... OPE i ...... OPE N )OPE N )and 1 ? i ? j ? N and N ? 3 and OPE i = OPE j DisjointObjectProperties( OPE 1 ... OPE N ) and 1 ? i ? N and N ? 2and 1 ? i ? N and N ? 2 DisjointObjectProperties( OPE i OPE j ) EquivalentObjectProperties( OPE 1 and i,j ? {1,N} and i ? j and N ? 2Year 2018InverseObjectProperties( OPE 1 OPE 2 )ObjectInverseOf( OPE 2 ) ) EquivalentObjectProperties( OPE 25IDGroup II V IV IIReplaced axiom EquivalentDataProperties DPE 1 ... DPE i ... DPE j ... DPE N ) and 1 ? i ? j ? N and N ? 3 and DPE i = DPE j EquivalentDataProperties( DPE 1 ... DPE N ) and 1 ? i ? N and N ? 2 EquivalentDataProperties( DPE 1 DPE 2 ) DisjointDataProperties( DPE 1 ... DPE i ... DPE j ... DPE N ) ObjectPropertyDomain( OPE CE ) ObjectPropertyRange( OPE CE ) FunctionalObjectProperty( OPE ) InverseFunctionalObjectProperty( OPE ) ReflexiveObjectProperty( OPE ) IrreflexiveObjectProperty( OPE ) SymmetricObjectProperty( OPE ) TransitiveObjectProperty( OPE )Replacing axiom(s) ObjectInverseOf( OPE 1 ) ) SubClassOf (Object Some Values From(OPE owl:Thing ) CE ) SubClassOf( owl:Thing ObjectAllValuesFrom( OPE CE ) ) SubClassOf( owl:Thing ObjectMaxCardinality( 1 OPE ) ) SubClassOf (owl:Thing ObjectMaxCardinality( 1 ObjectInverseOf( OPE ) ) ) SubClassOf( owl:Thing ObjectHasSelf( OPE ) ) SubClassOf( ObjectHasSelf( OPE ) owl:Nothing ) SubObjectPropertyOf( OPE ObjectInverseOf( OPE ) ) EquivalentDataProperties ( DPE 1 ... DPE i ... DPE N ) and 1 ? i ? N and N ? 2 EquivalentDataProperties( DPE i DPE j ) and i,j ? {1,N} and i ? j and N ? 2 SubDataPropertyOf( DPE 1 DPE 2 ) SubDataPropertyOf( DPE 2 DPE 1 ) DisjointDataProperties ( DPE 1 ... DPE i ... DPE N ) SubObjectPropertyOf (ObjectPropertyChain( OPE OPE ) OPE ) )Volume XVIII Issue II Version I ( ) C Global Journal of Computer Science and Technologyand 1 ? i ? j ? N and N ? 3 and DPE i = DPE jand 1 ? i ? N and N ? 2VDisjointDataProperties( DPE 1 ... DPE N ) and 1 ? i ? N and N ? 2DisjointDataProperties( DPE i DPE j ) and i,j ? {1,N} and i ? j and N ? 2IVDataPropertyDomain( DPE CE )SubClassOf( DataSomeValuesFrom (DPE rdfs:Literal ) CE )IVDataPropertyRange( DPE DR )SubClassOf( owl:Thing DataAllValuesFrom( DPE DR ) )IVFunctionalDataProperty( DPE )SubClassOf( owl:Thing DataMaxCardinality( 1 DPE ) )© 2018 Global Journals 4ID GroupReplaced axiomReplacing axiom(s) 5ID GroupReplaced data rangeReplacing data range(s)1III (3)2II3III (1)4II5III (1)6III (3)7III (3)8IIf) Class expressionsCardinality, ObjectMaxCardinality, ObjectExactCardinality,OWL 2 class expressions are constructed ofDataSomeValuesFrom, DataAllValuesFrom, DataHasValue,classes and properties. In structural specification [2] classDataMinCardinality, DataMaxCardinality and DataExactexpressions are represented by the ClassExpressionCardinality. In Table 6, the transformations of IDs: 9-14 andabstract class. The abstract class ClassExpression is19 are defined in [2], the other transformations are ourspecified by the following concrete classes: Class,proposal.ObjectIntersectionOf, ObjectUnionOf, ObjectComplementWe exclude two general cases from furtherOf, ObjectOneOf, ObjectSomeValuesFrom, ObjectAllValuesconsiderations -those of the existential and universalFrom,ObjectHasValue,ObjectHasSelf,ObjectMinclass expressions: 6The Method of Normalizing OWL 2 DL OntologiesID GroupReplaced class expressionReplacing class expression(s)1III (3)ObjectComplementOf (ObjectComplementOf( CE ) )CE2 3 4 5 6II III (1) II III (1) III (3)ObjectUnionOf( CE 1 ... CE i ... CE j ... CE N ) and 1 ? i ? j ? N and N ? 3 and CE i = CE j ObjectUnionOf (ObjectUnionOf( CE 1 ... CE Ai ... CE AN ) ... CE Bj ... CE BM ) ) and 1 ? i ? N and N ? 2 and 1 ? j ? M and M ? 2and 1 ? i ? N and N ? 2 ObjectIntersectionOf( CE 1 ... CE i ... CE N ) and 1 ? i ? N and N ? 2 ObjectIntersectionOf (CE 1 ... CE Ai ... CE AN ... CE Bj ... CE BM ) ) and 1 ? i ? N and N ? 2 and 1 ? j ? M and M ? 2 ObjectComplementOf (ObjectUnionOf( CE 1 ... CE N ) ) ObjectUnionOf( CE 1 ... CE i ... CE N ) and 1 ? i ? N and N ? 2 ObjectUnionOf (CE 1 ... CE Ai ... CE AN ... CE Bj ... CE BM ) ) and 1 ? i ? N and N ? 2 and 1 ? j ? M and M ? 2C ( ) Volume XVIII Issue II Version I 7 Year 20187 8 9 10 11 12 13 14 15III (3) II IV IV IV IV IV IV III (2)ObjectComplementOf (ObjectIntersectionOf( CE 1 ... CE N ) ) and 1 ? i ? N and N ? 2 ObjectOneOf( a 1 ... a i ... a N ) and 1 ? i ? N and N ? 1 ObjectMinCardinality( 1 OPE CE ) ObjectMaxCardinality (0 OPE ObjectComplementOf( CE ) ) ObjectSomeValuesFrom (OPE ObjectOneOf( a ) ) DataMinCardinality( 1 DPE DR ) DataMaxCardinality (0 DPE DataComplementOf( DR ) ) DataSomeValuesFrom (DPE DataOneOf( lt ) ) ObjectUnionOf (ObjectMinCardinality( n 1 OPE CE ) CE i ... CE N ) and 1 ? i ? N and N ? 2 and n 1 ? 0Global Journal of Computer Science and TechnologyObjectIntersectionOf16III (2)(ObjectMinCardinality( n 2 OPE CE ) CE i ... CE N )and 1 ? i ? N and N ? 2 and n 2 ? 017III (2)ObjectUnionOf (ObjectMaxCardinality( m 2 OPE CE )© 2018 Global Journals 6applied on the given axiom(4)EquivalentClasses(:FourLeafClover :FourLeafClover ObjectIntersectionOf(ObjectMinCardinality( 3 :hasLeaf :Leaf )ObjectMaxCardinality( 7 :hasLeaf :Leaf )ObjectIntersectionOf( ObjectMinCardinality( 4 :hasLeaf :Leaf )ObjectMaxCardinality( 4 :hasLeaf :Leaf ) ) )Rule 5 from Table 6 applied on (4)(5)EquivalentClasses( :FourLeafClover :FourLeafClover ObjectIntersectionOf(ObjectMinCardinality( 3 :hasLeaf :Leaf )ObjectMaxCardinality( 7 :hasLeaf :Leaf )ObjectMinCardinality( 4 :hasLeaf :Leaf )ObjectMaxCardinality( 4 :hasLeaf :Leaf ) ) )Rule 20 from Table 6 applied on (5)(6)EquivalentClasses( :FourLeafClover :FourLeafCloverObjectIntersectionOf( ObjectMaxCardinality( 7 :hasLeaf :Leaf )ObjectMinCardinality( 4 :hasLeaf :Leaf )ObjectMaxCardinality( 4 :hasLeaf :Leaf ) ) )Rule 23 from Table 6 applied on (6)(7)EquivalentClasses( :FourLeafClover :FourLeafCloverObjectIntersectionOf( ObjectMinCardinality( 4 :hasLeaf :Leaf )ObjectMaxCardinality( 4 :hasLeaf :Leaf ) ) )Steps 10-15 of the algorithm result in the following transformations:Rule 1 from Table 1 applied on (7)(8)EquivalentClasses( :FourLeafClover ObjectIntersectionOf(ObjectMinCardinality( 4 :hasLeaf :Leaf )ObjectMaxCardinality( 4 :hasLeaf :Leaf ) ) )Rule 2 from Table 1 applied on (8)SubClassOf( :FourLeafClover ObjectIntersectionOf(ObjectMinCardinality( 4 :hasLeaf :Leaf )ObjectMaxCardinality ObjectUnionOf(ObjectComplementOf( CE 1 )...ObjectComplementOf( CE N ) )is (16):(? ( ) C © 2018 Global Journals The Method of Normalizing OWL 2 DL Ontologies © 2018 Global Journals We have to show that (4) is correct. If we assume that ( 4) is false, it means that (5) is true: ?? ? (???? 1 ) ?? ? ?? ? (???? 2 ) ?? ? ?? ? (???? 1 ) ?? ? (???? 2 ) ?? It means that: (???? 1 ) ?? ? (???? 2 ) ?? ? ? We have received contradiction, which had to be proved. Proof 2 for construct replacements from The Method of Normalizing OWL 2 DL Ontologies VII. Proofs of the Correctness of the OWL 2 Construct Replacements This section aims at presenting proofs of correctness of the OWL 2 construct replacements presented in tables in Section 4. The replacing language constructs (right column in tables) are semantically equivalent to the replaced language constructs (left column in tables). The proofs are based on direct model-theoretic semantics [13]for OWL 2, which is compatible with the description logic SROIQ. The following convention is used: 1. V C is a set of classes containing at least the owl: Thing and owl: Nothing classes. 2. V OP is a set of object properties containing at least the object properties owl: topObjectProperty and owl: bottomObjectProperty. Proving equivalence comes down to the use of the interpretation definition and the rules of set theory. We selected two replacement rules for the proofs; all other ones could be proved analogically. ## Proof 1 for construct replacements from * OWL 2 Web Ontology Language Document Overview (Second Edition). W3C Recommendation 11 December 2012 * OWL 2 Web Ontology Language. Structural Specification and Functional-Style Syntax W3C Recommendation 11 December 2012 Second Edition * The Even More Irresistible SROIQ OHorrocks UKutz Sattler Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning AAAI Press 2006. 2006 * OWL 2 Web Ontology Language New Features and Rationale (Second Edition) W3C Recommendation 11 December 2012 * OWL 2 Web Ontology Language Profiles (Second Edition). W3C Recommendation 11 December 2012 * Semantic Validation of UML Class Diagrams with the Use of Domain Ontologies Expressed in OWL 2 MSadowska ZHuzar 2017 Springer International Publishing Software Engineering: Challenges and Solutions * Unified Modeling Language,Version 2.5, Doc. No: ptc OMG 2013-09-05 * A Prototype Tool for Semantic Validation of UML Class Diagrams with the Use of Domain Ontologies Expressed in OWL 2 MSadowska Towards a Synergistic Combination of Research and Practice in Software Engineering Cham Springer 2018 * How to design better ontology metrics VDenny YSure The Semantic Web: Research and Applications 2007 * Proceedings Workshop on Ontologies for Multiagent Systems (OMAS) in conjunction with European Knowledge Acquisition Workshop ALRector 2002 Normalisation of ontology implementations: Towards modularity, re-use, and maintainability * Modularisation of domain ontologies implemented in description logics and related formalisms including OWL ALRector Proceedings of the 2nd international conference on Knowledge capture the 2nd international conference on Knowledge capture ACM 2003 * MOF) Core Specification, version 2.0. Object Management Group Meta Object Facility * OWL 2 Web Ontology Language Direct Semantics (Second Edition) W3C Recommendation 11 December 2012