Imagine I have a property :loves that is not :Symmetric and I'm working in the following closed "space"
I can the express this idea in a pidgin of first order logic
which infers the new facts
Can I define this :mutallyLoves property in OWL?
EDIT: I'd be interested in seeing ways to materialize or query :mutallyLoves using other tools, like SPARQL, RIF, SPIN, whatever...
I think to do this in SPIN, you need to create your own sub class of rdf:Property. For example, my:DerrivedProperty. And your own property to say what property it is derived from. For example, my:derrivedFrom. Then you would say the following:
The following SPIN rule should create the inferences:
You can also throw in
This rule will work collaboratively with SPIN OWL RL rules for symmetricity
answered 07 Nov '11, 17:48
We can extend Signified's partial solution that uses a class :MutuallyLoved into a full solution for the property :mutuallyLoves, if we make two additional assumptions.
Firstly, and that's probably easy to accept, we state that if A mutually loves B, then A also (ordinarily) loves B:
Secondly, we only consider /true/ love, and, as we all know, true love can only be given to a /single/ person (at most):
Next, we "translate" the class of people who are mutually loved into the class of people who are mutually loving /someone/:
Now let's probe :Naoko's and :Sato's love! As :Naoko is a member of class :MutuallyLoved, there must be, via axiom (3), some Mr. X whom she :mutuallyLoves. Now, as we know from (1), to :mutuallyLoves people means to :loves them, so we know that :Naoko :loves Mr. X. And as :loves has been determined to be a functional relationship by (2), it turn's out from the premise that ":Naoko :loves :Sato" that Mr. X is, in fact, :Sato himself! Hence, there is no more reason to disbelieve in :Naoko's and :Sato's true love for each other:
Lovely story, isn't it! But what about reasoning?
The result is clearly too hard for the OWL 2 RL/RDF rules, with all the property restrictions and existential semantics being involved. I have checked with Ivan Herman's online RL reasoner, with all additional features turned on, and got a negative result.
The solution /is/ in the scope of the OWL 2 Direct Semantics when applied to the /unrestricted/ OWL 2 Structural Specification, but is unfortunately beyond OWL 2 DL, since already Signified's example is in conflict with one of the global restrictions of OWL 2 DL ("You shall not apply self-restrictions on properties defined by property chain axioms!"), and my three additional axioms above make the situation even worse. HermiT 1.3.2 does not confirm the entailment (wrongly claims non-entailment). Pellet 2.3.0 claims entailment, but only after several suspicious warnings that it will ignore diverse axioms while doing reasoning and that the conclusion ontology is empty, which is clearly not the case, so it seemed to be confused and only accidentally correct. Therefore, it turns out that using an OWL 2 DL reasoner is not a reliant method. The tests were made with this cleaned-up version of the whole example in RDF/XML:
However, the solution is, formally, in OWL 2 Full. I have checked it with our "naive" approach to OWL 2 Full reasoning presented in http://dx.doi.org/10.1007/978-3-642-22438-6_35 and it worked! I'm afraid, I still haven't a handy reasoner tool for people to easily play with themselves, but whoever is interested can copy and paste the TPTP code at
into any first-order theorem prover (see the link in the file there for FOL reasoners). That's a translation of the example here. The remaining stuff in the file is a sufficient selection of OWL 2 Full semantic conditions to make the example produce the result (the full set of semantic conditions would be a little too much and would be inefficient). Happy OWL 2 Full reasoning! :-)
This is conceptually the same problem as discussed here (aka. property intersection, role conjunction, etc.). The conclusion there is that it's not possible in OWL 2 DL, and probably not possible in OWL 2 Full.
However, you can use
From this, you can see that
...but (as far as we can tell), you cannot resolve the cyclical relationship between them using OWL 2. In summary, you can detect cyclical property paths in OWL 2, but you can (probably) only infer class memberships from such detections, not binary relations.
EDIT: just saw the comments on the answer. Doh! ...anyways, there's a little bit more detail here.