Reasoning about Semantic Web in Isabelle/HOL

13 years 7 months ago
Reasoning about Semantic Web in Isabelle/HOL
Semantic Web is regarded as the next generation of the World Wide Web. It provides not only the structure of the web but also meaningful semantics for the information presented. To make Semantic Web services understandable for distributed agents, formal definitions of the ontologies and their consistencies are essential. However, the existing tools for reasoning about Semantic Web ontologies are still primitive. We believe that mature Software Engineering tools, such as theorem provers, can contribute to the reasoning phase. In this paper, we present an approach of encoding the Semantic Web ontology (DAML+OIL) into the generic theorem prover Isabelle/HOL for automatic reasoning. Furthermore, a translation tool was developed to transform Semantic Web ontologies into their extended Isabelle theories. With additional intermediate lemmas, Isabelle can be used to perform both subsumption (class) level and instantiation (instance) level reasoning of the Semantic Web ontologies.
Yue Tang, Jin Song Dong, Jing Sun, Brendan P. Maho
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Authors Yue Tang, Jin Song Dong, Jing Sun, Brendan P. Mahony
Comments (0)