Institution Morphisms for Relating OWL and Z

Checking for properties of Web ontologies is important for the development of reliable Semantic Web systems. Software specification and verification tools can be used to complement the Knowledge Representation tools in reasoning about Semantic Web. The key to this approach is to develop sound transformation techniques from Web ontology to software specifications so that the associated verification tools can be applied to check the transformed specification models. Our previous work has demonstrated a practical approach to translating Web ontologies to Z specifications. However, from a sound engineering point of view, the translation is lacking the theoretical work that can formally relate the respective underlying logical systems of OWL and Z. In this paper, we take the advantage that the logics underlying OWL and Z can be represented as institutions and we show that the institution comorphism provides a formal semantic foundation for the transformation from OWL to Z.