owl - QCRs vs functional property

Question

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.

Answer 1

这三个公理

1. Man SubClassOf喝一些饮料
   
   • 男人⊑∃drinks.Beverage
2. 饮料：函数式、逆函数式
   
   • 东西 ⊑ ≤1 饮料。
   • 东西⊑ ≤1 饮料^{-1 . 东西}

在逻辑上不等同于

3. Man SubClassOf恰好喝了1 杯饮料
   • 男人⊑ =1 饮料。饮料

这是第一个模型中不一致的一些数据，但在第二个模型中没有：

m1 rdf: 类型 Man 。
d1 rdf：类型饮料。
d2 rdf:type（不是饮料）。
m1 喝 d1, d2 。

“属性p是功能性的”是等价于“Thing p max 1 Thing”的公理。

Answer 2

我相信这两个版本并不完全相同。如果drinks 是反函数的，那么两个喝同一种饮料的人会被推断为同一个人。在第二个版本中，情况并非如此（根据您的描述，我还没有检查本体）。

编辑：与 Dmitry Tsarkov（FaCT++ 的主要开发人员）讨论了这个问题。他评论说，功能特征相当于最大 1 基数。恰好 1 基数包括存在，这意味着推理器有不同的场景要探索，这会更复杂。我已经向他指出了这个问题，以提供更全面的答案。

Answer 3

在与丹尼斯进一步讨论后，他向我解释了这个问题。

基本上模型是正确的，但它需要实现每所房子的左/右最多有一个邻居。考虑情况：H5 左 H4 左 H3 左 H2 左 H1 和附加 H5 左 H3 在原始模型中这是不可能的，因为（逆）功能不允许它。（如果 H5 离开 H4，则 H5 离开 H3 是不可能的） 在我们的模型中，我们对 left_to/right_to 没有更多的限制。所以考虑的情况是有效的。

为了解决这个问题，我们需要再添加一条语句： House SubClassOf left_to max 1 House /or/ House SubClassOf right_to max 1 House

所以结果是：最大 1 = 功能性的 QCR，但模型错误。