I have question based on the topic:
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.
Thank you for your answers.
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.