Using Vampire to Reason with OWL

OWL DL corresponds to a Description Logic (DL) that is a fragment of classical first-order predicate logic (FOL). Therefore, the standard methods of automated reasoning for full FOL can potentially be used instead of dedicated DL reasoners to solve OWL DL reasoning tasks. In this paper we report on some experiments designed to explore the feasibility of using existing general-purpose FOL provers to reason with OWL DL. We also extend our approach to SWRL, a proposed rule language extension to OWL.

• Type: Conference
• Year: 2004
• Where: SEMWEB
• Authors: Dmitry Tsarkov, Alexandre Riazanov, Sean Bechhofer, Ian Horrocks
• Keywords: OWL DL, OWL DL Corresponds, OWL DL Reasoning, SEMWEB 2004