Clever Geek Handbook

QCRs versus functional property

I have a question based on the topic:

SOF - Einstein's puzzle in OWL

In owl, all power constraints are based on the functional and inverse functional properties of the object's properties. I redid it with QCR.

Old model (example):

man drinks some beverage;
drinks -> functional, inferse functional

New model / EDITED / :

man drinks exactly 1 beverage;
beverage drinkedBy exactly 1 man;
drinks -> domain:man, range:beverage
drinkedBy -> domain:beverage, range:man
drinks inverseOf drinkedBy

I've replaced all "some" with "exactly 1". I think the first type is equivalent to the second model, but the FaCT ++ argument is frozen after 15 seconds of running it (3+ GB of RAM lost and frozen). HermiT does not freeze, but it cannot output anything other than subclasses.

Final file / EDITED / : FS or MR

Thank you for your responses.

0


source to share


3 answers


After additional discussion with Denis, he explained the problem to me.

In principle, the model is correct, but it must be implemented so that each house has at most one neighbor on the left / right. Consider the situation: H5 left H4 on the left, H3 left H2 on the left, H1, and an additional H5 left H3 In the origin model it is impossible, because the (reverse) functional does not allow this. (If H5 left H4, it is impossible for H5 to leave H3) In our model, we no longer have left_to / right_to constraints. Thus, the situation in question is valid.



To solve this problem, we need to add another expression: House SubClassOf left_to max 1 House / or / House SubClassOf right_to max 1 House

So the result is: QCR with max 1 = functional but the model was wrong.

0


source


These three axioms

  • Man SubClassOf drinks some Drinks
    • Man & sqsubseteq; & Exist; drinks.Beverage
  • drinks: functional, reverse functional
    • Thing & sqsubseteq; & leq; 1 drinks.Thing
    • Thing & sqsubseteq; & leq; 1 drink -1 .Thing

not logically equivalent

  1. SubClassOf person will write exactly 1 drink
    • Man & sqsubseteq; = 1 drinks.Beverage


Here are some data that are inconsistent in the first model, but not in the second:

m1 rdf: type Human.
d1 rdf: beverage type.
d2 rdf: type (not drink).
m1 drinks d1, d2.

"The property p is functional" is the equivalent axiom to "Thing p max 1 Thing".

+4


source


I believe the two versions are not exactly equivalent. If the drinks are reverse functional, two people drinking the same drinking pattern are considered to be the same person. In the second version this is not the case (from your description I have not checked the ontologies yet).

Edit: discussed this with Dmitry Tsarkov (the main developer of FaCT ++). He noted that the performance is equivalent to maximum power. exactly 1 cardinality includes existence, that is, the intelligent has different tables to study, which would be more complicated. I pointed this question to him in order to give a more complete answer.

+2


source






More articles:


All Articles