# Non-standard Reasoning Services for the Verification of DAML+OIL Ontologies

Yingjie Song, Rong Chen

► To cite this version:

Yingjie Song, Rong Chen. Non-standard Reasoning Services for the Verification of DAML+OIL Ontologies. 6th IFIP WG 12.5 International Conference on Artificial Intelligence Applications and Innovations (AIAI), Oct 2010, Larnaca, Cyprus. pp.203-210, 10.1007/978-3-642-16239-8_28. hal-01060669

HAL Id: hal-01060669

https://inria.hal.science/hal-01060669v1

Submitted on 17 Nov 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Non-Standard Reasoning Services for the Verification
of DAML+OIL Ontologies

Yingjie Song, Rong Chen

School of Information Science & Technology.
Dalian Maritime University, Dalian 116026, P. R. China
{tiantian_yingjie@sina.com, tsmc.dmu@gmail.com}

**Abstract.** Ontology has a pivot role in the development of Semantic Web which provides the understanding of various domains that can be communicated between people and applications. Motivated by J. S. Dong's work, we propose a new approach to interpreting DAML+OIL in a lightweight modeling language for software design, Alloy, which is used to provide a non-standard reasoning service for the verification of DAML+OIL ontologies. To do so, Jena is first used to parse ontology documents into classes, properties and statements, next we use algorithms to translate them into Alloy model, the Alloy Analyzer is then used to check and reason about such model. The experiments show that our method greatly improves J. S. Dong's work, and distinguishes from the traditional ontology reasoners in property checking and reasoning.

**Keywords:** Ontology Reasoning; DAML+OIL; Alloy; Semantic Web

# 1 Introduction

A Semantic Web [4], as the next generation of the Web, provides well-defined notations and techniques for humans and applications to quickly and accurately access Web information and services. In the development of Semantic Web there is a pivot role of ontology, since ontology languages provide modeling primitives for converting notations in nature language into machine-readable logical formulas, from which autonomous software agents may infer and come to conclusions [1].

Ontology languages, such as DAML+OIL, enhance computer programs through structured organizational information and rules, with which it is able to understand the logical relationship between them. Ontology reasoning is crucial in that inconsistent ontology cannot be shared or used by autonomous software agents. A number of ontology inference engines, such as FaCT [3], RACER [2], and FaCT++ [10] have been developed with the advancement of ontology languages to facilitate ontology creation, management, verification, merging, etc. However, the checking and reasoning of complex ontology-related properties cannot be done by them.

There is a role for software engineering techniques and tools that contribute to the Semantic Web development. J. S. Dong first proposes the use of Alloy [5] in checking and reasoning about the semantic relationship between web resources [1]. We propose a novel transformation from DAML+OIL ontology to Alloy, which greatly improves J. S. Dong's work; our approach scales up well and can work on a larger scope of property checking.
The rest of the paper is organized as follows: Section 2 gives a brief introduction to DAML+OIL and Alloy. In the section 3, a simple ontology example is given described in DAML+OIL, and then the ontology document is analyzed by jena, the results of which will be used as the inputs of the algorithms, which are used to transferred the DAML+OIL into Alloy model.

# 2 Overview of DAML+OIL and Alloy

## 2.1 Logical Characteristic of DAML+OIL

DAML+OIL [7] is a successor language to DAML [8] and OIL [9] that builds on earlier W3C standards such as RDF, RDF Schema, and the language components of OIL. DAML+OIL layered on top of RDFS it inherited RDFS ontological primitives (subclass, range, domain). As a semantic Web ontology language, DAML+OIL provides users a richer set of modelling primitives (transitivity, cardinality, ...) that are commonly found in frame-based languages.

Although DAML+OIL is tightly integrated with RDFS, which provides the only specification of the language and its only serialization, DAML+OIL defines the semantic of the language to give a meaning to any ontologies that conform to the RDFS specification, including “strange” constructs such as slot constraints with multiple slots and classes. It contains richer modeling primitives than RDF. This is made easier by the fact that the semantics of DAML+OIL is directly defined in both a model-theoretic and an axiomatic form. Theoretically, DAML+OIL is undecidable, but its processor to detect the occurrence of constraints and warn the user of the consequences.

## 2.2 Alloy

Alloy [5] is a textual, declarative modelling language rooted in first order relational logic, which is widely accepted as micromodels of software in the software engineering community. For relationships between web resources are focus point in the Semantic Web, we believe that it will be a new application domain for Alloy. An Alloy model consists of *Signatures*, *Relations*, *Facts*, *Functions* and *Predicates*. *Signatures* represent the entities of a system and *Relations* are used to describe relations between such entities. *Facts* and *Predicates* introduce constraints over such *Signatures* and *Relations*. Whereas *Facts* are constraints to be always valid, *Predicates* are named parameterized contraints for depicting operations, *Functions* are named expression with parameters that return results.

Alloy comes with a tool, the Alloy Analyzer [6], which supports fully automated analysis of Alloy models through simulation and *Assertion* checking. While *Assertion* are assumptions about the model that can be checked. Simulation yields a random instance that is consistent with the model. Given a user specified scope on the model elements bounding the domain, the analyzer first translates an Alloy model into boolean formulas, and then invokes a SAT-solver to find an instance. If an instance that violates the assertion is found within the scope, the assertion is not valid and the instance is returned as a counterexample.
# 3 Description of the Approach

The specific process of our approach on ontology reasoning is shown in Fig.1: ontology documents are analyzed by Jena, and the results contain three parts: Classes C, Property P and Statements S. Next, the results are converted into Alloy model using daml2Alloy algorithm. And then we use Alloy Analyzer to check the model. In case an error, we check back the original ontology and correct it accordingly. The jena is used again to check the corrected ontology. These three steps are explained in more detail in the following.

<figure><img src="image_2.png" /><figcaption>Fig.1. The specific process of ontology reasoning.</figcaption></figure>

## 3.1 Parsing DAML+OIL Documents

To handle DAML+OIL ontologies, we adopt Jena [10] as a frontend of our framework to parse textual DAML+OIL documents. Jena provides APIs for manipulating RDF graphs, abstracting from which it provides the ontology API for OWL and DAML ontologies. Our DAML+OIL parser, based on Jena parser, reads a DAML+OIL document of animal ontology (shown in Fig.2), which defined four classes: Animal, Male, Man and Female. While Man is subclass of Male, Male and Female are disjointed subclasses of Animal. hasFather, hasParent and hasChild are three properties such that hasParent and hasChild are inverse to each other and hasFather is subproperty of hasParent. We translate it into RDF triples, which are composed of *Classes, Properties and Statements*.

<figure><img src="image_3.png" /><figcaption>Fig.2. A DAML+OIL document of animal ontology</figcaption></figure>
We use a simple ontology about animal as a running example to show the outputs of Jena. It contains a sequence of *Classes*, *Properties* and *Statements*, each having a couterpart in the original document. Such *Classes*, *Properties* and *Statements* provide programmatic objects like DAMLClass, DAMLProperty and RDFTriples for our conversion algorithm in the next section. As illustrated in Fig. 1, our DAML+OIL parser reads such a textual document and converts it into RFD triples as follows:

<figure><img src="image_4.png" /><figcaption>Fig. 3. Jena outputs of “Animal” ontology</figcaption></figure>

<figure><img src="image_5.png" /></figure>

## 3.2 Generation of the Alloy Model

Given RDFTriples and the related classes, we move on to generate the equivalent Alloy model, which contains Alloy classes and the relationship between them.

As shown below, our Algorithm daml2Alloy (C, P, S, Σ) converts the input *Classes* (denoted as C), *Properties* (denoted as P) and *Statements* (denoted as S) into a textual Alloy model Σ. To do so, we map each class into an Alloy signature, and the relationships between such classes are represented by Alloy primitives such as *Relations*, *Facts*, *Functions* and *Predicates*.

**Algorithm 1:** daml2Alloy (C, P, S, Σ)

**Input:** a set *C* of *Classes*, a set *P* of *Properties* and a set *S* of *Statements*

**Output:** a textual Alloy model Σ

1. $\Sigma \leftarrow \omega$;

2. FOR each $c \in C$

3. $\Sigma \leftarrow \Sigma + 2\text{Alloy}(c, S)$;

4. FOR each $s \in \Sigma$

5. IF $s$.**predicate.name** = "disjointWith"

6. IF $s$.**subject.subClassOf** ≠ $s$.**object.subClassOf**

7. $\Sigma \leftarrow \Sigma + \text{"pred \{no c1:" + $s$.**subject.name** +", c2:" + $s$.**object.name** +" | c1 = c2\}"}$;

8. IF $s$.**predicate.name** = "complementOf"

9. $\Sigma \leftarrow \Sigma + \text{"pred \{" + $s$.**subject.name** +" =" + $C - s$.**object.name** +"\}"}$;

10. IF $s$.**predicate** meets one of Conditions in Table 3

11. the corresponding generated Alloy predicate is appended to $\Sigma$

12. RETURN $\Sigma$;

In our algorithm, the Alloy model Σ is initialized to be an empty string ω on line 1, each class c is converted into a signature by invoking 2Alloy (c, S) algorithm (see below), next follows the conversion of each statement into *Predicates* in a loop through lines 4~11, finally the produced model Σ is returned. Since each statement
use parent (property) to represent the parent property of the parameter property. Note that the calculation of the range of a property with respect to Statements is quite similar to Algorithm 3, we omit it for obviousness.

<figure><img src="image_6.png" /></figure>

Taking the “Animal” ontology as an example again, it is used to show how the conversion is achieved. The DAML+OIL document will be transferred into Alloy model as Fig.4.

<figure><img src="image_7.png" /><figcaption>**Fig. 4.** The generated Alloy model of “Animal” ontology</figcaption></figure>

<figure><img src="image_8.png" /></figure>

## 3.3 Verifying Ontologies with the Alloy Analyzer

Semantic Web reasoning is one of key issues for ontology design, construction and maintenance, which contains the ontology consistency checking, subsumption reasoning, which task is to derive a class is another’s parent, and implication relation checking. The correct ontology required to meet at least on instance. This is achieved through Alloy Analyzer to generate an instance of the model in given scope. As shown in Figure 5, there is an inconsistency occurred in the “Animal” model. This is because there is a subProperty constraint between femaleHasFather and animalHasFather, Woman is subClassOf Male is implied since Male is the range of animalHasFather and Woman is the range of femaleHasFather.

<figure><img src="image_9.png" /><figcaption>**Fig. 5.** Checking result of Alloy Analyzer</figcaption></figure>
Note that if Alloy Analyzer can't find a solution, it maybe for the too small scope. If there is something of inconsistent in reasoning with Alloy, assertion is an important criterion. When Alloy Analyzer can't find a counterexample, the assertion is reasonable, else Alloy Analyzer will generate a counterexample and some predicates and facts should be added to improve the model.

## 4 Comparison of Experimental Results

In J. S. Dong's article, classes and properties in semantic ontology were converted to subclasses of resource, and then predicates were used to establish the relationship between different resources. As a proof tool of program correctness, theorem machine prove and knowledge representation, the shortcoming of first order logic is that in reasoning it prone to "combinatorial explosion". Method we used is to make use of the characteristics of Alloy, we convert the properties of the semantic ontology to the properties of the signature in Alloy model. It has been greatly improved in the scale. Table 4 shows the operation results in the case of the same scope of the two methods.

<table><caption>**Table 4 Comparison of Experimental Data**</caption><thead><tr><th rowspan="2"></th><th rowspan="2">scope</th><th colspan="4">GenerateCM + GeneratePM</th><th colspan="4">J. S. Dong</th></tr><tr><th>vars</th><th>primary vars</th><th>clauses</th><th>time</th><th>vars</th><th>primary vars</th><th>clauses</th><th>time</th></tr></thead><tbody><tr><td rowspan="4">Family</td><td>(5)</td><td>1074</td><td>135</td><td>1674</td><td>32</td><td>3025</td><td>265</td><td>7875</td><td>47</td></tr><tr><td>(10)</td><td>3168</td><td>520</td><td>5281</td><td>63</td><td>15530</td><td>1430</td><td>44475</td><td>156</td></tr><tr><td>(30)</td><td>27468</td><td>4560</td><td>48201</td><td>391</td><td>257182</td><td>30090</td><td>806831</td><td>4828</td></tr><tr><td>(40)</td><td>48618</td><td>8080</td><td>85861</td><td>578</td><td>570992</td><td>69320</td><td>1810146</td><td>14688</td></tr><tr><td rowspan="4">Course</td><td>(10)</td><td>5477</td><td>440</td><td>11868</td><td>63</td><td>11845</td><td>1440</td><td>31357</td><td>125</td></tr><tr><td>(20)</td><td>17507</td><td>1680</td><td>41626</td><td>203</td><td>67632</td><td>9480</td><td>197133</td><td>859</td></tr><tr><td>(30)</td><td>38737</td><td>3720</td><td>93696</td><td>453</td><td>204687</td><td>30120</td><td>612883</td><td>3578</td></tr><tr><td>(40)</td><td>69887</td><td>6560</td><td>171406</td><td>813</td><td>460162</td><td>69360</td><td>1396873</td><td>8812</td></tr><tr><td rowspan="4">airportCode</td><td>(5)</td><td>1196</td><td>125</td><td>1910</td><td>16</td><td>2416</td><td>270</td><td>5573</td><td>31</td></tr><tr><td>(20)</td><td>14716</td><td>1700</td><td>26300</td><td>156</td><td>67758</td><td>9480</td><td>193719</td><td>1109</td></tr><tr><td>(35)</td><td>44656</td><td>5075</td><td>81200</td><td>688</td><td>44656</td><td>5075</td><td>81200</td><td>5781</td></tr><tr><td>(50)</td><td>90796</td><td>10250</td><td>166250</td><td>1422</td><td>866928</td><td>13200</td><td>2627124</td><td>17422</td></tr><tr><td rowspan="4">Document</td><td>(10)</td><td>11458</td><td>1800</td><td>19691</td><td>125</td><td>31271</td><td>2070</td><td>87236</td><td>375</td></tr><tr><td>(20)</td><td>37528</td><td>6000</td><td>67371</td><td>422</td><td>169783</td><td>10740</td><td>535897</td><td>2172</td></tr><tr><td>(30)</td><td>80318</td><td>12600</td><td>146711</td><td>1125</td><td>501543</td><td>32010</td><td>1655392</td><td>6860</td></tr><tr><td>(40)</td><td>139108</td><td>21600</td><td>256451</td><td>2235</td><td>1109903</td><td>71880</td><td>3750587</td><td>31016</td></tr></tbody></table>

As is shown in Table 4, we analyze and compare with several ontologies. Variables, primary variables, clauses and runtime are the four mainly elements for comparison. For each ontologies, we give four scopes to illustrate that with the expansion of the scope, our approach reflects the increasingly better performance comparing to the method of article [1].

The first ontology we used is the Family ontology, which contains three classes and five properties. Its Alloy model is composed of three signatures, five properties and one predicate. As is shown in Table 4, with the scope increasing, the advantages are more and more obvious. When the scope is equal to 40, the number of variables is 10 times larger than ours, the number of primary variables is more than 8 times and the runtime is 25 times. It is the similar with the other examples.
# 5 Conclusion

We propose an approach to convert the DAML+OIL ontology to Alloy model, and then using the Alloy Analyzer to automatically check and reason the generated model. First, we use Jena to analyze the ontology document and get classes, properties and statements of it. Next, we propose two algorithms to generate the Alloy model of the ontology. Finally, the tasks of checking and reasoning are executed by Alloy Analyzer. We have applied our approach to several ontologies, it can discover errors and inconsistencies, and when there are something wrong, we can efficiently correct the errors on the assistance of the counterexample given by Alloy Analyzer.

# 6 Acknowledgments

This work is supported by National Natural Science Foundation of China (60775028), the Major Projects of Technology Bureau of Dalian No.2007A14GXD42, and IT Industry Development of Jilin Province.

# References

1. Hai Wang Jin Song Dong, Jing Sun. Checking and reasoning about semantic web through alloy. In Proceedings of Formal Methods Europe: FME'03, 2805 of Lect.:796--814, 2003.

2. Volker Haarslev and Ralf Möller. RACER User's Guide and Reference Manual: Version 1.7.6, Dec 2002.

3. Ian Horrocks. The fact system. In TABLEAUX '98: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 307--312, London, UK, 1998. Springer-Verlag.

4. J.Hendler T.Berners-Lee and O.Lassila. The semantic web. Scientific American, May 2001.

5. Daniel Jackson. Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol., 11 (2):256--290, 2002.

6. Daniel Jackson, Ian Schechter, and Hya Shlyahter. Alcoa: the alloy constraint analyzer. In ICSE '00: Proceedings of the 22nd international conference on Software engineering, pages 730--733, New York, NY, USA, 2000. ACM.

7. Ian Horrocks, Peter F. Patel-Schneider, and Frank van Harmelen. Reviewing the design of daml+oil: an ontology language for the semantic web. In Eighteenth national conference on Artificial intelligence, pages 792--797, Menlo Park, CA, USA, 2002. American Association for Artificial Intelligence.

8. F.van Harmelen, P. F. Patel-Schneider, and I. Horrocks (editors). Reference description of the daml+oil ontology markup language. March, 2001.

9. Jeen Broekstra, Michel Klein, Stefan Decker, Dieter Fensel, and Ian Horrocks. Adding formal semantics to the web building on top of rdf schema. In In Proc. of the ECDL 2000 Workshop on the Semantic Web, 2000.

10. Dmitry Tsarkov and Ian Horrocks. Fact++ description logic reasoner: System description. In In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006, pages 292--297. Springer, 2006.

11. Lutz C. The complexity of reasoning with concrete domains revised version. Technical report, 1999.