Warning:
This wiki has been archived and is now read-only.
FullSemanticsInversePropertyExpressions
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)