FullSemanticsInversePropertyExpressions

From OWL
Jump to: navigation, search

Goto OWL 2 Full Semantics Page


The OWL 2 Full semantics of anonymous inverse property expressions.

In addition to inverse property axioms, which are expressed by means of owl:inverseOf in OWL 1, OWL 2 additionally introduces the concept of an inverse property expression for specifying "inlined" anonymous inverses of properties. The RDF syntax of inverse property expressions reuses the URI 'owl:inverseOf'. The difference is that the subject of this property is a bNode instead of a URI.

No special treatment in OWL 2 Full needed

The distinction between URIs and bNodes on the LHS of owl:inverseOf does not effect OWL 2 Full. The original semantic condition for owl:inverseOf covers this extended usage, too.

The triple '_:p owl:inverseOf q' has a bNode in subject position, which means that the subject is an existentially quantified variable. This means that there exists some property p, for which (p,q) ∈ EXT_I(S_I(owl:inverseOf)) holds. Since the semantic condition for owl:inverseOf axioms universally quantifies on the LHS and RHS of owl:inverseOf triples, the semantic condition in particular applies to these two variables p and q.

General scheme:

 ∀x: A(x) → B(x)
 ∃y: A(y)
 ---------------
 ∃y: B(y)

Goto OWL 2 Full Semantics Page