The correctness of the Z semantics of OWL is the theoretical foundation of using software engineering techniques to verify Web ontologies. As OWL and Z are based on different logical systems, we use institutions to represent their underlying logical systems and use institution morphisms to prove the correctness of the Z semantics for OWL DL. Categories and Subject Descriptors F.4 [MATHEMATICAL LOGIC AND FORMAL LANGUAGES]: Miscellaneous; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods--Representation languages General Terms Languages, Theory, Verification Keywords OWL, Z, institution, comorphism of institutions