Comparing OWL Semantics

Turner, David ; Carroll, Jeremy J.

HP Development Company

关键词: OWL;    semantic web;   

RP-ID  :  HPL-2007-146

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

The OWL Web Ontology Language is endowed with two model theories, reflecting its origins as a compromise between two different communities. By design these model theories give rise to very similar semantics, and a precise statement of the correspondence between the model theories is conjectured with a sketch proof at the end of the OWL semantics specification document. We have filled in the details of this sketch proof using the Isabelle/HOL proof assistant, and developed machinery for further study of the formal semantics of OWL. Our study was sufficiently detailed to find a handful of minor errors in the specification of the semantics of OWL that previous work had overlooked. We also sought a stronger result by showing a partial converse to the known correspondence, but it proved impossible to achieve this within our time constraints; instead we conjecture a possible method for strengthening the correspondence. 21 Pages