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.
