Owlready2中"only"约束类型的异常表现及推理逻辑疑问

问题场景 #

在Owlready2中构建本体后，运行HermiT推理器出现两个异常结果：

1. Equipment个体被错误归类为Task；
2. Task类被推断为与Thing等价。
   将约束中的only替换为some后，推理结果符合预期。此外，用户提供的简化示例在HermiT下会得出类与Thing等价，但用Protege的ELK推理器无此推论。以下是相关代码示例：

原始代码 #

class Equipment(Thing): pass

class Task(Thing): pass
class EquipmentTask(Task): pass

class task_executed_by_equipment(EquipmentTask >> Equipment, FunctionalProperty): pass
class task_included_subtasks(Task >> Task): pass

class EquipmentTask(Task): equivalent_to = [task_executed_by_equipment.exactly(1, Equipment)]
class MainTask(EquipmentTask): equivalent_to = [task_included_subtasks.only(EquipmentTask)]

task = Task(task_executed_by_equipment=Equipment())
sync_reasoner()

简化示例代码 #

class P(ObjectProperty): domain=[C]
class C(Thing): equivalent_to = [P.only(C)]

核心逻辑解析 #

1. allValuesFrom（only）的真实含义 #

全称约束P only C的逻辑本质是：如果个体x拥有属性P的某个取值y，那么y必须是C的实例。

• 关键误区：很多人误以为only要求个体必须有属性P的取值，但实际上，如果个体没有任何P属性的取值，它依然满足这个约束。这与some（存在约束）完全不同，some要求个体至少有一个符合条件的P属性取值。
• 举MargheritaPizza的例子：MargheritaPizza ≡ Pizza ∧ hasTopping only (Mozzarella ∨ Tomato)，按OWL逻辑，一个没有任何配料的披萨也属于玛格丽特披萨，因为它没有违反“所有配料都是芝士或番茄”的约束。

2. 简化示例的推理过程 #

对于简化代码中的C ≡ P.only(C)：

• 对于任意Thing个体x：
  • 若x没有P属性的取值，x满足P.only(C)，因此被归类为C的实例；
  • 若x有P属性的取值，根据P的domain是C，x本身已经是C的实例。
• 综上，所有Thing都是C的实例，HermiT因此推断C ≡ Thing。
• ELK推理器基于EL描述逻辑，EL对全称约束的“空满足”场景不做此类推论，所以不会得出C与Thing等价的结果。

3. 原始代码的异常原因 #

• MainTask的约束漏洞：MainTask等价于task_included_subtasks.only(EquipmentTask)，任何Task个体只要没有task_included_subtasks属性，就满足该约束，会被推断为MainTask实例。
• domain约束的连锁反应：task_executed_by_equipment的domain是EquipmentTask，用户创建的Task实例被赋值了该属性，根据domain约束，这个实例会被推断为EquipmentTask的实例。
• 全称约束的泛化：由于“空满足”特性，所有Thing个体（包括Equipment）只要没有违反Task相关的约束，都会被推断为Task的实例，最终导致Task ≡ Thing，Equipment个体被错误归类到Task中。

4. 替换为some后正常的原因 #

some是存在约束，要求个体必须至少有一个符合条件的属性取值，不存在“空满足”的情况。比如task_included_subtasks.some(EquipmentTask)要求MainTask必须包含至少一个EquipmentTask子任务，只有满足该条件的个体才会被归类到MainTask，不会无限制扩大范围。

内容的提问来源于stack exchange，提问作者pfp.meijers