Infrastructure

One of the targeted application combines the semantic web with transformation system engineering. In the framework of the semantic web, knowledge will be independently described by different organisations in different ways. These organisations will need to combine knowledge originating from hererogeneous sources. It is thus necessary to transform knowledge before using it. The safety of the transformations must then be ensured.

This drives us directly to a framework in which transformations from one representation language to another are available from the network and proofs of various properties of these languages are attached to them. It is noteworthy that transformations and proofs do not have to come from the same origin. They can even be produced by the application client.

The transformation system engineer can gather these transformations and their proofs, check the proofs before importing them in its transformation development environment. She will then be able to create a new transformation flow and generate the proofs of the properties that she requires. Finally, she will be able to publish the transformation and its proof on the network.

This same framework applies with knowledge transformation. Indeed, if knowledge is expressed in the same language it is not necessarily expressed in the same modelling style: the ontologies can be dramatically different. To that extent, it is necessary to find the correspondences between these ontologies and take advantage of these correspondences (for transforming for instance).

In the same extent as before, alignments can be published on the web, together with some assertions of properties and exploited for transforming or merging knowledge.

The components of such an infrastructure are presented here.

Transformation flow language and processor

In order to prove or check the properties of transformations, it is necessary to have a representation of these transformations. The XSLT language enables the expression of a transformation in XML but is relatively difficult to analyse. In order to overcome that problem, we have designed and developed, in collaboration with the FluxMedia company, the Transmorpher environment. Transmorpher allows the expression of complex transformation flows.

Transmorpher enables the definition and processing of transformations of XML documents by composing other transformations. It describes the transformation flows in XML. Input/output channels carry the information, mainly XML, from one transformation to another. Transmorpher provides a set of abstract elementary transformations (including their execution model) and one default instantiation. Such elementary transformations include external call, e.g., XSLT, dispatcher, serializer, query engine, iterator, merger, generator and rule sets.

An extension of Transmorpher towards safer transformations consists of attaching assertions to the transformations in a transformation flow in order to tell if a property is assumed, proved or to be checked. This will allow real experimentation of proving properties of compound transformations.

Alignment infrastructure

Alignment are more intelligible than transformations: they only express correspondences between ontology entities. This can be the basis for studying their properties (moreover, these properties can also be inferred from the methods used for generating alignments). In addition, from an alignment, it is possible to generate a transformation. So ontology alignments are natural candidates for expressing ontology-dependent transformations [Euzenat 2008a].

We have developed an alignment exchange format and Alignment API [David 2011a] which enable the communication of ontology alignments on the network. It also provides a number of features such as the ability to compose alignments and to generate transformations from alignments.

We aim at using the Alignment API and implementation as a facility for communicating alignments on the web. Several potential uses of this facility are currently under study including:

• Composing semantic web services, in which alignments are used for generating input/output transformations (called ontology mediators) that are used for composing web services together;
• Communication in multi-agent systems, in which the alignment service can be contacted by an agent for aligning two ontologies and translating messages; moreover, alignments can be negociated through argumentation;
• Matching context in ambient computing which consists of finding the information about the current situation by using the various devices available in the environments (sensors as well as other integrated services); since the description of the devices cannot be known in advance, it is necessary to fetch it and very often to translate it in the current application ontology;
• Using semantic peer-to-peer systems which consists of querying for information and resources to a network of peers which are all described in autonomous ontologies; in this situation the queries (and sometimes the answers) must be translated from peer to peer.

Services that are necessary in such an infrastructure are:

• The ability to store alignments, whether they are provided by automatic means or by hand;
• The proper annotation of these alignments in order for the clients to evaluate the opportunity to use such an alignment or to start from it (this starts from the information about the algorithms that generate the alignments, the reasons for them that can be used in agent argumentations, as well as proved properties of the alignments);
• The ability to produce alignments on the fly through various algorithms that can be extended and parameterised;
• The ability to generate knowledge processors such as transformations, translators, rules as well as to process these processors if necessary;
• The possibility to find similar ontologies and to contact other alignment servers in order to ask them for alignments that the current service cannot provide by itself.

Composition of properties and proof-checking

Proof carrying transformations

In a web context, transformations, their properties and their proofs can be made available on the network. Knowing the semantics of languages and the proofs of the transformation enables the application of the "proof-carrying code" idea [Necula 1998]. Consequently, the user can be sure that the result of the transformation is the transcription of the initial knowledge with the desired properties.

In order to check the proof of semantic properties, like (1) and (2), it is necessary to have (a) a representation of the transformation, (b) a specification of the semantics of languages (or of pattern specifications) and (c) a representation of the proof. These three elements will have to be developed in order to communicate and check proofs:

• For representing transformation, we use Transmorpher. One of the goals of this language is to embed the XSLT language in order to ease transformation composition and analysis.
• DSD is a language under development for describing the semantics (in model theory) of representation languages. It is based on MathML, Xpath and XSLT. This language will be tested on several knowledge representation formalisms.
• Proof representation (such proof by induction can be easily checked) is yet to be developed. Such a representation should take advantage of works for mathematics on the web such as MathML and OpenMath as well as more adapted ones like OMDoc [Kohlhase 2000].

We have experimented with the semantics description language in the definition of DLML (so that a DSD is automatically provided with each language from the semantics of individual constructors). We have built a few proof examples, mainly equivalence proofs, in description logics. They should be a good first example for testing concepts. We are preparing the proof of model preservation of the OWL to RDF transformation that we have written.