0

I have question based on the topic:

SOF - Einstein puzzle in OWL

In the owl, all cardinality restrictions are based on functional and inverse functional properties of Object Properties. I have remodeled it using QCRs.

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 replaced all "some" with "exactly 1". I think the first type is equivalent to the second model, but reasoner FaCT++ is frozen after 15 sec of his start (3+ GB RAM wasted and frozen). HermiT is not freezing, but he cannot infer anything but subclasses.

Final file /EDITED/: FS or MR

Thank you for your answers.

Community
  • 1
  • 1
Michal Joštiak
  • 161
  • 9
  • Did you make any progress with this? – Joshua Taylor Oct 13 '14 at 14:07
  • Nope. I post it to protege-user mailing list (without answer) and here [link](https://groups.google.com/forum/#!forum/hermit-users) but it was deleted without getting me a reason. – Michal Joštiak Oct 14 '14 at 06:22
  • "cannot infer anything but subclasses." This may be a silly question, but (I'm assuming you're using the DL query pane), you did check the appropriate checkboxes on the right hand side? – Joshua Taylor Oct 14 '14 at 10:58
  • What is the query that you're trying to answer? – Joshua Taylor Oct 14 '14 at 10:59
  • I used individual tab. Here are links with different reasoning results : With result - [link](http://i62.tinypic.com/33ue44z.jpg) Without result - [link](http://i57.tinypic.com/10mr22o.jpg) – Michal Joštiak Oct 15 '14 at 06:32

3 Answers3

4

These three axioms

  1. Man SubClassOf drinks some Beverage
    • Man ⊑ ∃drinks.Beverage
  2. drinks : Functional, InverseFunctional
    • Thing ⊑ ≤1 drinks.Thing
    • Thing ⊑ ≤1 drinks-1.Thing

are not logically equivalent to

  1. Man SubClassOf drinks exactly 1 Beverage
    • Man ⊑ =1 drinks.Beverage

Here's is some data that's inconsistent in the first model, but not in the second:

m1 rdf:type Man .
d1 rdf:type Beverage .
d2 rdf:type (not Beverage) .
m1 drinks d1, d2 .

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

Joshua Taylor
  • 84,998
  • 9
  • 154
  • 353
  • Y thats true. In this puzzle one man has one pet, house with color and so on. So I used exactly. But if I used max instead of exactly the result is same. The problem should be with inverse functional, as Ignazio mentioned. – Michal Joštiak Sep 24 '14 at 13:14
  • Also property drinks has domain and range. – Michal Joštiak Sep 24 '14 at 13:26
2

I believe the two versions are not exactly equivalent. If drinks is inverse functional, two men drinking the same instance of drink are inferred to be the same man. In the second version, that's not the case (from your description, I have not checked the ontologies yet).

Edit: discussed this with Dmitry Tsarkov (main developer for FaCT++). He remarked that a functional characteristic is equivalent to max 1 cardinality. exactly 1 cardinality includes existence, meaning the reasoner has a different tableaux to explore, which would be more complex. I've pointed him to this question to provide a more comprehensive answer.

Ignazio
  • 10,504
  • 1
  • 14
  • 25
  • Good point. But it has no impact on the result. I mark all properties as inverse functional and used them as "max 1" but reasoner cannot solve it. – Michal Joštiak Sep 24 '14 at 13:30
  • I cannot see why the result would be different, once the inverse functional is in - probably you have triggered a code path that's not very optimised (for FaCT++) and might be a bug (for FaCT++ and HermiT alike). – Ignazio Sep 24 '14 at 17:35
  • I discussed it with the author of the base model, Denis Ponomaryov. He said that the model is correct too, but "you forgot to add more information about left_to/right_to roles. You are using QCR's for them in the axioms: --12. Kools are smoked in the house next to the house where the horse is kept. 15. The Norwegian lives next to the blue house-- but this appears to be not enough to solve the riddle, because you still need left_to/right_to to be functional." But I dont know why. I try it and it works. But why OP right/left must be functional ? Dunno. – Michal Joštiak Nov 18 '14 at 07:15
0

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

Basically model is correct, but its need to implement that each house has max one neighbour on the left/right. Consider situation: H5 left H4 left H3 left H2 left H1 and additional H5 left H3 In origin model its not possible because (inverse) functional not allow it. (If H5 left H4, its not possible to H5 left H3) In our model, we have no more restriction on left_to/right_to. So the considering situation is valid.

To solve this problem we need to add one more statement: 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.

Michal Joštiak
  • 161
  • 9
  • Who is Denis? How did you go from beverages to houses? Why did you not accept Joshua's answer, which seems very concise? – Jim L. Sep 13 '17 at 13:58
  • Read others comments. Denis Ponomaryov autor of the origin model. Joshua answer is OK, but not related to the puzzle specification. – Michal Joštiak Sep 29 '17 at 06:28