Exmo: Assessing Semantic Properties of Knowledge Transformations
by Jérôme Euzenat
Sharing knowledge on the Semantic Web will require the transformation and adaption of knowledge to client needs. The complexity of the representations to be transformed can hide the effects of transformations, though the use of knowledge dictates them. Exmo aims to provide tools for characterising the action of these transformations in syntactic, semantic or semiotic terms.
Approaching semantically defined knowledge on the Web is not the end of interoperability problems. Indeed, knowledge providers use different languages, axiomatic or conventions for expressing knowledge. Importing knowledge in the context of different applications will require adapting it to the target context (language, axiomatic or convention). This adaptation can be processed a priori or on the fly and the transformation involved can be automatically or manually generated.
The action of these transformations ranges from minor syntactic formatting to complex processing such as deducing consequences and generalising them. It is important for applications to be confident of the properties of these transformations. These properties can be related to the syntax (eg correct expression of the result in a particular language), the semantics (eg preservation of the meanings of knowledge by the transformation) or the pragmatics (eg preservation of the reader's interpretation by transformation). They may also concern the transformation processing (eg correct termination) or its results (eg loss of information in the result).
One of the goals of the Exmo action is to assess the properties satisfied by transformations. This objective requires:
- the capacity to analyse transformations into units assembled by precise constructors
- the knowledge of properties that can characterize transformations and their behaviour with regard to the constructors
- the opportunity to prove properties from elementary transformations.
Exmo deals with these three problems and aims to build an environment in which users can compose transformations and formally characterise their properties.
In collaboration with the Fluxmedia company we developed the Transmorpher environment that allows the composition of XML transformations. The unit transformations are either expressed in XSLT (in which case the properties are asserted) or in a simplified rule transformation language (from which properties can be assessed). These transformations can be composed in subroutine, sequence, parallel or loops which constitute the main constructors of the system. The environment is portable and freely available (see Figure).
|Screenshot of the Transmorpher graphic environment.
The transformations developed within Transmorpher will have to be annotated by the properties that they satisfy. In particular we are investigating semantic properties (tied to the model theoretic semantics of the languages involved) and their relations (eg interpretation-preservation implies consistency-preservation). These properties have been applied to an XML encoding of description logics and this effort should be reiterated in the next W3C-proposed languages.
The next step consists in providing Transmorpher users with tools for proving the properties of a particular transformation. Our current efforts use the relations between properties in order to establish the minimal properties enjoyed by the composition of Transmorpher constructors. We would also like to experiment with proof checkers for the inductive proofs often used for proving the equivalence of languages.
In the context of the Web, and of the Semantic Web infrastructure, transformations could be made available for many other parties that might want to integrate them within their own processes. In order to establish the properties satisfied by the resulting transformation, it will be necessary to be able to assess those of the gathered transformations. For that reason, we want to extend the system presented above with the capability of importing and exporting transformations, their properties and, if available, the proofs of these properties. The importers would then be able to check the proofs and thus trust the properties of the imported transformations. This is an instantiation of 'proof-carrying code' to transformations.
Besides classical properties tied to the syntax and semantics of the representations, the overall goal of Exmo is to be able to take into account properties tied to their pragmatics, such as the rhetoric of a discourse or the semiotic interpretations of readers. For instance, this would enable us to establish that the same impact is provided by a multimedia presentation before and after its transformation. This requires investigations into the field of semiotics.
Jérôme Euzenat, INRIA
Tel: +33 476 61 53 66