QCR 与功能特性

Question

我有一个基于主题的问题：

SOF - Einstein puzzle in OWL

在 owl 中，所有基数限制都基于 Object Properties 的泛函和反泛函性质。我已经使用 QCR 对其进行了改造。

旧型号（示例）：

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

新模型/EDITED/：

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

我将所有“一些”替换为“正好 1”。 我认为第一种类型相当于第二种模型，但是推理器 FaCT++ 在他开始 15 秒后被冻结（浪费和冻结了 3+ GB RAM）。 HermiT 并没有被冻结，但他只能推断出子类。

最终文件/EDITED/： FS 或 MR

感谢您的回答。

Answer 1

这三个公理

1. 男人 SubClassOf 喝 一些 饮料
   
   • 男人 ⊑ ∃drinks.Beverage
2. 饮料：功能性、逆功能性
   
   • 事物 ⊑ ≤1 杯饮料。东西
   • 事物 ⊑ ≤1 杯饮料^-1.东西

在逻辑上不等价于

1. 男人 SubClassOf 喝确切 1 饮料
   • 男人 ⊑ =1 饮料。饮料

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

m1 rdf:type Man .
d1 rdf:type Beverage .
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 /或/ House SubClassOf right_to max 1 House

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