Institution Morphisms for Relating OWL and Z

Checking for properties of Web ontologies is importantfor the development of reliable Semantic Web systems. Softwarespecification and verification tools can be used tocomplement the Knowledge Representation tools in reasoningabout Semantic Web. The key to this approach is to developsound transformation techniques from Web ontologyto software specifications so that the associated verificationtools can be applied to check the transformed specificationmodels. Our previous work has demonstrated a practicalapproach to translating Web ontologies to Z specifications.However, from a sound engineering point of view, the translationis lacking the theoretical work that can formally relatethe respective underlying logical systems of OWL andZ. In this paper, we take the advantage that the logics underlyingOWL and Z can be represented as institutions andwe show that the institution comorphism provides a formalsemantic foundation for the transformation from OWL to Z.