知识推理

小象实战讲义 · 知识图谱

知识图谱不是一张画完就固定的图。RDF 三元组摆进图里的事实、RDFS 和 OWL 写进本体里的概念层次与约束，都只是显式知识；水面之下还有大量”没有明说、但按语义必然成立”的知识：地产公司是公司、公司是法人实体，融创中国当然也是法人实体；一个人执掌一家公司，他就是股东；同一人执掌的两家公司之间应当存在关联交易。把这些隐含知识”算”出来，就是知识推理。本节先讲 OWL 为什么能支撑推理（描述逻辑与形式语义），再梳理四大标准推理任务与非标准的辩解，然后逐一讲透四类主流方法——Tableaux、Datalog 改写、查询重写、产生式规则——及代表工具，最后用 Python（rdflib）把原课 Jena/RDFox/Drools 实践的机制重跑一遍。本节讲的是逻辑推理，结论由形式语义保证正确，与给关系预测打概率分的统计推理是两条路线。

💡 核心导读

• OWL 是知识图谱语言中最规范、最严谨、表达能力最强的语言：RDF 语法为外壳、描述逻辑为内核。注意须限定为 OWL DL：它（及 OWL 2 DL）是一阶谓词逻辑的可判定子集；而不加约束的 OWL Full 与一阶逻辑同等不可判定。
• 知识库由 TBox（概念与关系的公理）和 ABox（个体的断言）构成，对应数据库的 schema 与 data；“解释”把概念映射成论域子集、关系映射成二元组集合，这就是 OWL 语义的数学定义。
• 推理任务分四类标准任务（可满足性、分类、实例化、不一致性检测）与非标准的辩解；前四者产出新知识或质量报告，辩解回答”结论凭什么推出”。
• 四类方法各有分工：Tableaux 面向可满足性与分类；Datalog 改写把公理变成规则做前向物化；查询重写（OBDA）在查询时把 SPARQL 展开成 SQL、数据不动；产生式规则用”匹配—冲突解决—执行”循环驱动业务动作。
• 这些机制都能用 rdflib 复现：上下位推理、类别补全、自定义规则、不一致检测，本节给出可运行的最小实现。

一、描述逻辑：OWL 本体推理的逻辑基础

1.1 为什么推理要从 OWL 讲起

RDF 给了三元组（主体、谓词、客体）统一数据结构，RDFS 给了 subClassOf、subPropertyOf、domain、range 这批基础词汇，OWL 则在其上提供了丰富得多的语义词汇。课件对 OWL 的定位是：知识图谱语言中最规范、最严谨、表达能力最强；基于 RDF 语法，文档具有语义理解的结构基础；促进统一词汇表、丰富语义词汇；允许逻辑推理。“规范”来自 W3C 标准；“严谨”和”能推理”同出一源：OWL 的逻辑基础是描述逻辑（Description Logic, DL），它是一阶谓词逻辑的可判定子集——对”本体有没有矛盾""苹果算不算创新企业”这类问题，存在算法能在有限时间内给出确定答案，一阶逻辑整体则只是半可判定的。表达能力与复杂度始终要取舍：描述逻辑家族通过挑选构造算子，把表达能力控制在”既能刻画常见本体结构、推理又可判定”的范围内。OWL 仍用 RDF 三元组语法，再复杂的类定义也会被拆成一条条三元组。课件例子：声明 Jack 是”是人但不是父母”的个体，即 Person ⊓ ¬Parent 的实例：

@prefix : <http://example.org/dl#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .

:Jack a [ owl:intersectionOf ( :Person [ owl:complementOf :Parent ] ) ] .

方括号是匿名节点（空白节点），代表匿名复合类；owl:intersectionOf 后是一个 RDF 列表，第一个成员是 :Person，第二个成员是用 owl:complementOf 指向 :Parent 的匿名类（即”非 Parent”）。推理机面对的不是数学符号，而是三元组搭起来的语法树。

1.2 描述逻辑系统的四个组成部分

一个描述逻辑系统有四个基本组成：基本元素——概念（concept）、关系（role）、个体（individual）；TBox 术语集；ABox 断言集；以及建立在二者之上的推理机制。三种基本元素的集合论解释是整套语义的地基：概念解释为论域子集，如 { x | Student(x) }，对应一元谓词；关系（角色 role）解释为论域上的二元关系，即笛卡尔积的子集（二元组集合），如 { (x, y) | friend(x, y) }，对应二元谓词；个体是论域中的具体实例，如小明（Ming），对应一阶逻辑里的常量。

知识库分两个盒子。TBox（Terminological Box，术语盒）存放关于概念和关系的泛化知识，称公理（Axiom）：先引入名称（Mother、Person、has_child），再声明它们的关系，如包含公理 Mother ⊑ ∃has_child.Person（母亲一定有一个孩子，且孩子是人）。公理不是”绝对真理”，而是对领域概念关系的明确约定，在约定范围内作为推理依据。ABox（Assertion Box，断言盒）存放关于特定个体的外延断言：概念断言如 Mother(Alice)、Person(Bob)，关系断言如 has_child(Alice, Bob)，知识库记作 K = (T, A)。二者分工可类比关系数据库：TBox 相当于 schema（表、字段、外键约束），ABox 相当于 data（一条条记录）。工程中”搭图谱”搭出来的往往主要是 ABox，TBox 常被忽略，却恰恰是推理的依据；TBox 规模通常不大、由专家与工程师人工构建、成本可控，ABox 才可能达到数十亿条规模——“TBox 人工建不现实”是常见误解，真正大的是数据。

1.3 解释、模型与逻辑蕴含：推理为什么是”对”的

公理和断言凭什么能推出新结论？靠严格的语义。描述逻辑用”解释（interpretation）“定义语义，记作 I，由两部分组成：非空集合 Δ^I，称论域；解释函数 ·^I 把个体名映射成论域元素、概念映射成论域子集、关系映射成二元关系集合——解释就是把符号映射到”所指对象集合”。复合概念通过集合运算递归定义，课件构造算子语义表：

注意 ∀R.C：若 x 没有 R 邻居，“所有 R 邻居都属于 C”在逻辑上空真（vacuously true），没有孩子的人也属于 ∀has_child.Doctor；∃R.C 则要求至少一个满足条件的邻居，没有孩子的人不属于它。

在解释之上定义模型：若 C^I ⊆ D^I，称 I 满足公理 C ⊑ D，记作 I ⊨ C ⊑ D，R ⊑ S 同理；对断言，a^I ∈ C^I 则 I ⊨ C(a)，(a^I, b^I) ∈ R^I 则 I ⊨ R(a,b)。一个解释满足 K 中每条公理和断言，它就是 K 的一个模型。由此有三个核心概念：知识库可满足指 K 至少存在一个模型；概念可满足指存在模型使 C^I 非空；逻辑蕴含（entailment）指断言 σ 在 K 的每个模型中都成立，记作 K ⊨ σ，推理机的任务就是找出所有这样的 σ。这套语义给了逻辑推理两个统计推理给不了的保证：正确性（soundness）——结论在每个模型中都成立、一定对；完备性（completeness）——语义上蕴含的结论算法都能推出。对比之下，链路预测（link prediction）补关系只输出概率、可能对也可能错，subClassOf 链必然得出的结论则可以打包票。下面代码把”解释”落成可运行程序，并用 rdflib 解析 Jack 的 RDF 结构：

# -*- coding: utf-8 -*-
# 代码块1：把描述逻辑的"解释"落成代码——在有限论域上计算概念的集合扩展
from rdflib import Graph, Namespace, RDF, OWL
from rdflib.collection import Collection

# 一个解释 I = (论域 Δ, 解释函数)：原子概念解释成子集，角色解释成二元组集合
domain = {"Jack", "Alice", "Bob", "Carol"}
concepts = {
    "Person": {"Jack", "Alice", "Bob", "Carol"},
    "Parent": {"Alice", "Bob"},        # 有孩子的人
    "Male": {"Jack", "Bob"},
    "Doctor": set(),
}
roles = {
    "hasChild": {("Alice", "Jack"), ("Bob", "Carol")},
}

def extent(expr):
    """递归计算概念表达式在该解释下的集合扩展（对应课件语义表）"""
    tag = expr[0]
    if tag == "atom":                                  # 原子概念 C^I
        return set(concepts[expr[1]])
    if tag == "and":                                   # 合取 C ⊓ D -> C^I ∩ D^I
        return extent(expr[1]) & extent(expr[2])
    if tag == "or":                                    # 析取 C ⊔ D -> C^I ∪ D^I
        return extent(expr[1]) | extent(expr[2])
    if tag == "not":                                   # 否定 ¬C -> Δ^I 去掉 C^I
        return domain - extent(expr[1])
    if tag == "exists":                                # 存在 ∃R.C
        r, ce = expr[1], extent(expr[2])
        return {x for x in domain for y in domain if (x, y) in roles[r] and y in ce}
    if tag == "forall":                                # 全称 ∀R.C（没有 R 邻居的个体也满足）
        r, ce = expr[1], extent(expr[2])
        out = set()
        for x in domain:
            nbr = [y for y in domain if (x, y) in roles[r]]
            if all(y in ce for y in nbr):
                out.add(x)
        return out
    raise ValueError(expr)

print("Person ⊓ ¬Parent =", sorted(extent(("and", ("atom", "Person"), ("not", ("atom", "Parent"))))))
print("∃hasChild.Male =", sorted(extent(("exists", "hasChild", ("atom", "Male")))))
print("∀hasChild.Doctor =", sorted(extent(("forall", "hasChild", ("atom", "Doctor")))))

# 用 rdflib 解析课件中的 Jack 声明：Jack 是 Person ⊓ ¬Parent 这个匿名复合类的实例
g = Graph()
g.parse(data="""
@prefix : <http://example.org/dl#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
:Jack a [ owl:intersectionOf ( :Person [ owl:complementOf :Parent ] ) ] .
""", format="turtle")
EX = Namespace("http://example.org/dl#")
for cls in g.objects(EX.Jack, RDF.type):
    for lst in g.objects(cls, OWL.intersectionOf):
        for member in Collection(g, lst):
            comp = list(g.objects(member, OWL.complementOf))
            if comp:
                print("RDF 结构：交集的第 2 个成员是匿名类，owl:complementOf 指向",
                      comp[0].toPython().split("#")[-1], "（即 ¬Parent）")
            else:
                print("RDF 结构：交集的第 1 个成员是原子概念",
                      member.toPython().split("#")[-1])

运行结果：Person ⊓ ¬Parent 扩展为 {Carol, Jack}，与”是人且没有孩子”的直觉一致；∃hasChild.Male 只含 Alice（她的孩子 Jack 是男性）；∀hasChild.Doctor 含 {Carol, Jack}——两人都没有孩子，全称量词空真成立，正对应 1.3 节强调的 ∃ 与 ∀ 的差别。

二、描述逻辑与 OWL 词汇的对应

2.1 公理词汇：描述逻辑记号如何写成 OWL 三元组

描述逻辑公理记号与 OWL 的 RDF 词汇一一对应（课件表格用早期词汇名，括号内为现行 OWL 2 标准词汇名）：

概念构造子同样有标准对应（均为 owl 命名空间）：⊓→intersectionOf、⊔→unionOf、¬→complementOf、枚举 {a,b,c}→oneOf、∃R.C→someValuesFrom、∀R.C→allValuesFrom、∃R.{v}→hasValue、≥nR/≤nR/=nR→minCardinality/maxCardinality/cardinality。每个算子在 RDF 层都有确定的三元组树结构，推理机读到词汇即知按哪种集合运算。

2.2 表达能力的分层：OWL 子语言与 OWL 2 Profile

允许的算子越多表达能力越强，但推理复杂度越高，某些组合甚至让可判定性丧失。OWL 早期分 Lite、DL、Full 三档（Full 放弃可判定性，DL 保证可判定，Lite 更弱更快）；OWL 2 又定义三个易处理的 Profile（子轮廓），各自面向一类方法：OWL 2 QL 面向查询重写，本体层薄、数据留在关系库，查询可重写成 SQL 高效执行；OWL 2 RL 面向规则，能用 Datalog 类规则实现的部分被单独切出，RDFox、GraphDB 主要支持它；OWL 2 EL 面向超大概念层次（如医学本体 SNOMED CT），分类可在多项式时间完成，本节不展开。记住这层对应就抓住了四类方法的适用边界：Tableaux 处理 OWL DL 全算子（可判定描述逻辑的完整部分），规则方法处理 RL，查询重写处理 QL。

三、知识推理的任务：四大标准任务与辩解

课件把推理定义为”通过各种方法获取满足语义的新知识或结论”：Page16 列出四个标准任务——可满足性、分类、实例化、不一致性检测；Page32 另把辩解列为 OWL 本体非标准推理（调试用），本节一并讲解。

3.1 可满足性（satisfiability）

分两个层面。本体可满足性检查本体是否有模型——找不到自洽解释让所有公理断言同时成立，本体即不一致。概念可满足性检查是否存在模型使该概念解释非空——若一个概念在所有模型里都只能解释为空集，它就不可满足，即定义自相矛盾、不可能容纳个体。课件例子：Man ⊓ Woman ⊑ ⊥（⊥ 是空概念），同时又有 Man(Allen) 和 Woman(Allen)，Allen 撑爆这条公理，本体没有模型。

3.2 分类（classification）：在 TBox 上算新概念包含关系

分类针对 TBox：由显式包含公理计算隐含的概念包含关系、补全概念层次，如由心肌梗塞 ⊑ 心脏病 ⊑ 疾病补出心肌梗塞 ⊑ 疾病。注意它与机器学习分类完全不同：机器学习分类是给个体打标签（ABox 层预测），描述逻辑分类是推导概念间的从属（TBox 层演绎）。课件用苹果公司例子演示多步分类，本体有四条公理：

Apple ⊑ ∃beInvestedBy.(Fidelity ⊓ BlackStone)   苹果由富达和黑石共同投资
∃beFundedBy.Fidelity ⊑ InnovativeCompanies      借助富达融资的公司是创新企业
∃beFundedBy.BlackStone ⊑ InnovativeCompanies    借助黑石融资的公司是创新企业
beInvestedBy ⊑ beFundedBy                       接受投资即是获得融资

推理链：由第一条，苹果存在一个”既是富达又是黑石”的投资方，因而存在富达投资方，即 Apple ⊑ ∃beInvestedBy.Fidelity；再由第四条把存在量词里的关系换成上位关系，得 Apple ⊑ ∃beFundedBy.Fidelity；最后套第二条公理得 Apple ⊑ InnovativeCompanies。每一步都是集合包含的传递，没有概率成分。

3.3 实例化（materialization）：在 ABox 上算新实例

实例化针对 ABox：计算属于某概念或关系的所有实例集合，分两种——新的类实例信息，如 Mother(Alice) 加 Mother ⊑ Woman 推出 Woman(Alice)；新的二元关系，如 has_son(Alice, Bob) 加 has_son ⊑ has_child 推出 has_child(Alice, Bob)。materialization 也译”物化”，即把推出的事实写回知识库，4.2、4.3 节会与”查询时重写”对照。兼并重组套利策略认为与大盘股兼并重组的上市企业有很高预期收益，课件用此例说明推理机能替代人工筛选条件，形式化后：

∃merge.BigCapital ⊑ ValueSecurity     与大盘股兼并重组的公司是高预期标的
SZ50 ⊑ BigCapital                      上证50 成分股属于大盘股
HS300 ⊑ BigCapital                     沪深300 成分股属于大盘股
SZ180 ⊑ HS300                          上证180 成分股属于沪深300
merge(SZ300377, SH600570)              赢时胜与恒生电子在区块链业务上兼并
SZ180(SH600570)                        恒生电子是上证180 成分股

推理链：SZ180(SH600570) 经 SZ180 ⊑ HS300、HS300 ⊑ BigCapital 两跳推出 BigCapital(SH600570)；配合 merge(SZ300377, SH600570) 得 ∃merge.BigCapital(SZ300377)；最后由第一条公理得 ValueSecurity(SZ300377)——赢时胜在该策略下是高预期标的。这本质是消息面套利，层层嵌套的选股筛选被推理机自动完成。

3.4 不一致性检测（inconsistency detection）

知识库在演化中不断进入新事实，若没有不相交性（disjointness）约束，矛盾归类会一直潜伏。课件例子：A、B 分别代表”心脏病”和”脑科疾病”，声明 A disjointWith B（等价 A ⊓ B ≡ ⊥）；若把”心内膜炎”同时归为 A、B 的实例就出现不一致。检测这类冲突是提升知识库质量的重要环节，与 3.1 互为表里。

3.5 辩解（justification，非标准推理）：结论是凭什么推出来的

推理机一次推出成百上千条结论，某条错了怎么定位病根？计算辩解：原始本体中能解释该结论的一个最小公理集。课件例子：分类后发现错误结论 Meningitis ⊑ ∃has-loc.Heart（脑膜炎发生在心脏，荒谬）；计算辩解发现病根是错误公理 Meningitis ⊑ HeartDisease（脑膜炎被错归为心脏病），改后错误结论消失。辩解是调试本体的核心手段，也是逻辑推理相对黑盒统计模型的优势：每条结论都有可复核的前提链。下面代码在 rdflib 上一次做完分类、实例化、辩解，为新结论记录前提并打印 Person(Alice) 的辩解链。

# -*- coding: utf-8 -*-
# 代码块2：分类、实例化与辩解——课件 Page24 的 Mother/has_son 例子
from rdflib import Graph, Namespace, RDF, RDFS, URIRef

FAM = Namespace("http://example.org/fam#")
g = Graph()
g.bind("fam", FAM)
g.parse(data="""
@prefix fam: <http://example.org/fam#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
fam:Mother rdfs:subClassOf fam:Woman .
fam:Woman rdfs:subClassOf fam:Person .
fam:has_son rdfs:subPropertyOf fam:has_child .
fam:Alice rdf:type fam:Mother .
fam:Alice fam:has_son fam:Bob .
""", format="turtle")

def name(t):
    return t.toPython().split("#")[-1]

def closure(node, rel):
    """沿 rel 关系求传递闭包"""
    seen, stack = set(), [node]
    while stack:
        cur = stack.pop()
        for nxt in rel.get(cur, ()):
            if nxt not in seen:
                seen.add(nxt); stack.append(nxt)
    return seen

# 先建两张 TBox 关系表
sub_class, sub_prop = {}, {}
for c, d in g.subject_objects(RDFS.subClassOf):
    sub_class.setdefault(c, set()).add(d)
for p, q in g.subject_objects(RDFS.subPropertyOf):
    sub_prop.setdefault(p, set()).add(q)
for p in list(sub_prop):  # 属性层级也求闭包
    for q in list(sub_prop[p]):
        sub_prop[p] |= sub_prop.get(q, set())

# 任务一·分类（TBox 层面）：计算新的概念包含关系
print("== 分类：Mother 的所有上位概念 ==")
for t in sorted(closure(FAM.Mother, sub_class), key=str):
    print("   Mother ⊑", name(t))

# 任务二·实例化（ABox 层面）：补全实例类型，同时记录辩解
def chain_paths(node, rel):
    """沿 rel 的原始公理边求路径，返回 {可达节点: [依次经过的 (起点, 终点) 边]}"""
    paths, stack = {}, [(node, [])]
    while stack:
        cur, edges = stack.pop()
        for nxt in rel.get(cur, ()):
            if nxt not in paths:
                paths[nxt] = edges + [(cur, nxt)]
                stack.append((nxt, edges + [(cur, nxt)]))
    return paths

just = {}   # 结论 -> (规则名, 前提列表)
for inst in set(g.subjects(RDF.type, None)):
    for c in set(g.objects(inst, RDF.type)):
        for sup, edges in chain_paths(c, sub_class).items():
            concl = (inst, RDF.type, sup)
            # 辩解只引用原始本体公理：1 条实例断言 + 链上每条原始 subClassOf 公理
            prems = [(inst, RDF.type, c)] + [(a, RDFS.subClassOf, b) for a, b in edges]
            just.setdefault(concl, ("subClassOf 实例化规则", prems))
            g.add(concl)
print("== 实例化：Alice 的全部类型 ==")
for t in sorted(g.objects(FAM.Alice, RDF.type), key=str):
    print("   Alice rdf:type", name(t))

# 实例化续：subPropertyOf 补全关系 has_son(Alice,Bob) -> has_child(Alice,Bob)
print("== 实例化：关系补全 ==")
for p, qs in sub_prop.items():
    for s, o in g.subject_objects(p):
        for q in qs:
            g.add((s, q, o))
            print(f"   {name(s)} {name(q)} {name(o)}  <- {name(p)} ⊑ {name(q)}")

# 任务三·辩解：解释 Person(Alice) 这条结论是怎么推出来的
print("== 辩解：Person(Alice) 的前提链 ==")
def explain(concl, depth=0):
    print("  " * depth + f"{name(concl[0])} rdf:type {name(concl[2])}")
    if concl in just:
        rule, prems = just[concl]
        print("  " * depth + f"  <- {rule}")
        for p in prems:
            print("  " * depth + f"     前提：{name(p[0])} {name(p[1])} {name(p[2])}")
explain((FAM.Alice, RDF.type, FAM.Person))

运行后：分类给出 Mother ⊑ Woman、Mother ⊑ Person；实例化把 Alice 的类型补成 {Mother, Woman, Person}，并由 has_son ⊑ has_child 补出 has_child(Alice, Bob)；辩解输出 Person(Alice) 的原始公理链——Alice rdf:type Mother、Mother rdfs:subClassOf Woman、Woman rdfs:subClassOf Person，三条前提全部来自原始本体，不含推出的三元组。

四、四类本体推理方法与工具

4.1 基于 Tableaux 运算的方法

适用场合是检查本体可满足性与实例检测。基本思想：从初始 ABox 出发，用规则不断扩展 ABox 直到结构完备，扩展中若出现冲突（clash）即判定不可满足，思路类似一阶逻辑的归结反驳（refutation）：想证明 Allen 不是 Woman，就把反面结论 Woman(Allen) 加进 ABox，推出矛盾则反面不成立、原命题得证。课件以主要 DL 算子给出 Tableaux 规则（初始 ABox 记作 A，迭代到不再变化）：

⊓+ 规则：若 C⊓D(x) 在 A 中，且 C(x)、D(x) 不在 A，则把 C(x)、D(x) 加入 A（合取拆开）
⊓− 规则：若 C(x)、D(x) 都在 A，且 C⊓D(x) 不在 A，则把 C⊓D(x) 加入 A（合取合并）
∃  规则：若 ∃R.C(x) 在 A，且不存在 y 使 R(x,y)、C(y) 都在 A，则新引入个体 y，
         把 R(x,y)、C(y) 加入 A（存在量词要求造一个新个体）
∀  规则：若 ∀R.C(x) 与 R(x,y) 都在 A，且 C(y) 不在 A，则把 C(y) 加入 A
⊑  规则：若 C(x) 在 A 且 TBox 中有 C⊑D，且 D(x) 不在 A，则把 D(x) 加入 A
⊥  规则：若 ⊥(x) 出现在 A（x 同时属于两个不相交概念），则拒绝 A

推演 Allen 例子。TBox：Man ⊓ Woman ⊑ ⊥；ABox：Man(Allen)，问 Allen 是否属于 Woman。把待反驳结论 Woman(Allen) 加入，初始 ABox 为 {Man(Allen), Woman(Allen)}；用 ⊓− 规则合成 Man ⊓ Woman(Allen)；再用 ⊑ 规则由 Man ⊓ Woman ⊑ ⊥ 得 ⊥(Allen)；最后 ⊥ 规则发现冲突、拒绝 ABox，反驳成功，Allen 不在 Woman 中。反过来，若 Woman(Allen) 本就写在原本体里，冲突无需假设就必然出现，说明本体本身不可满足。∃ 规则会”造出新个体 y”，是开放世界假设的体现——存在量词只承诺”有这么个对象”，不承诺是已知个体。正确性用 Herbrand 模型论证：Tableaux 构建出的 ABox 本质是本体的一个 Herbrand 模型，与本体任意模型的一个子集同构——算法拒绝它（推出冲突）等于拒绝所有模型，本体必然不可满足；无法拒绝时它本身就是模型，这同时保证了正确性与完备性。基于 Tableaux 的经典推理机四款：FaCT++（曼彻斯特大学，C++，可与 Protégé 集成，Java 版叫 JFact）；Racer（美国 Franz Inc.，商用，较早支持个体推理）；Pellet（马里兰大学开发、后由 Clark & Parsia 维护，Java，开源双许可含 AGPL，支持 OWL 2 DL 加规则与本体调试）；HermiT（牛津大学，Java，开源 LGPL，首个直接推理 OWL 2 DL 的推理机）。下面实现教学版 Tableaux，覆盖 ⊓+、⊓−、⊑、⊥ 四条规则，跑通 Allen 反驳与普通包含：

# -*- coding: utf-8 -*-
# 代码块3：迷你 Tableaux 推理机（实现课件 Page35 的核心规则，跑通 Page36-45 的 Allen 例子）
BOTTOM = "⊥"

def canon(c):
    """合取规范化（排序），避免 (A,B) 与 (B,A) 重复"""
    if isinstance(c, tuple) and c[0] == "and":
        parts = sorted([canon(c[1]), canon(c[2])], key=str)
        return ("and", parts[0], parts[1])
    return c

def fmt(c):
    """概念表达式转可读串"""
    if isinstance(c, tuple) and c[0] == "and":
        return f"{fmt(c[1])}⊓{fmt(c[2])}"
    return str(c)

def tableaux(tbox, abox):
    """tbox: [("gci", 左概念, 右概念)]；abox: [("isa", 个体, 概念)]。
    迭代使用 ⊓+ / ⊓− / ⊑ / ⊥ 规则扩展 ABox，直到完备或出现冲突。"""
    ab = {("isa", x, canon(c)) for (_, x, c) in abox}
    log = []
    for _ in range(20):
        progressed = False
        for x in {xx for (k, xx, c) in ab if k == "isa"}:
            cs = {c for (k, xx, c) in ab if k == "isa" and xx == x}
            # ⊓+ 规则：C⊓D(x) 在，则补 C(x)、D(x)
            for c in list(cs):
                if isinstance(c, tuple) and c[0] == "and":
                    for part in (c[1], c[2]):
                        if ("isa", x, part) not in ab:
                            ab.add(("isa", x, part)); progressed = True
                            log.append(f"⊓+规则：{c[1]}⊓{c[2]}({x}) -> 补 {part}({x})")
            cs = {c for (k, xx, c) in ab if k == "isa" and xx == x}
            # ⊓− 规则：两个原子概念同时成立，合成合取（教学版只合并原子概念）
            atoms = sorted([c for c in cs if isinstance(c, str)], key=str)
            for i in range(len(atoms)):
                for j in range(i + 1, len(atoms)):
                    conj = canon(("and", atoms[i], atoms[j]))
                    if ("isa", x, conj) not in ab:
                        ab.add(("isa", x, conj)); progressed = True
                        log.append(f"⊓−规则：{atoms[i]}({x})、{atoms[j]}({x}) -> {conj[1]}⊓{conj[2]}({x})")
            cs = {c for (k, xx, c) in ab if k == "isa" and xx == x}
            # ⊑ 规则：C(x) 在且 C⊑D，则补 D(x)；右端是 ⊥ 时直接产生冲突
            for (_, lhs, rhs) in tbox:
                lhs = canon(lhs)
                if lhs in cs and ("bot", x) not in ab:
                    if rhs == BOTTOM:
                        ab.add(("bot", x)); progressed = True
                        log.append(f"⊑规则：{fmt(lhs)}⊑⊥ 且 {fmt(lhs)}({x}) 成立 -> ⊥({x})")
                    elif ("isa", x, canon(rhs)) not in ab:
                        ab.add(("isa", x, canon(rhs))); progressed = True
                        log.append(f"⊑规则：{fmt(lhs)}({x}) 且 {fmt(lhs)}⊑{rhs} -> 补 {rhs}({x})")
        # ⊥ 规则：出现 ⊥(x) 即 clash，拒绝当前 ABox
        for tup in list(ab):
            if tup[0] == "bot":
                log.append(f"⊥规则：⊥({tup[1]}) 出现，当前 ABox 被拒绝")
                return False, log
        if not progressed:
            break
    return True, log

# 例子一：Man ⊓ Woman ⊑ ⊥，已知 Man(Allen)，问 Allen 是否属于 Woman？
tbox = [("gci", ("and", "Man", "Woman"), BOTTOM)]
abox = [("isa", "Allen", "Man"), ("isa", "Allen", "Woman")]  # 把待反驳结论 Woman(Allen) 加入
ok, log = tableaux(tbox, abox)
for line in log:
    print(line)
print("反驳后 ABox 是否无冲突：", ok)
print("=> 推出冲突，反驳成功，Allen 不在 Woman 中；若 Woman(Allen) 本就在原本体，则本体不可满足")
print()

# 例子二：普通包含推理 Man ⊑ Person，无冲突
ok2, log2 = tableaux([("gci", "Man", "Person")], [("isa", "Allen", "Man")])
for line in log2:
    print(line)
print("可满足（无冲突），且已补全 Person(Allen)：", ok2)

4.2 基于逻辑编程改写的方法：Datalog 规则推理

第二类方法把描述逻辑本体改写成逻辑程序（Datalog 规则），用规则引擎做前向推理。先讲边界：Datalog 规则本质是 Horn 子句，无法直接处理 ∃、∀、¬、⊔——∃ 要凭空造新个体，而 Horn 规则只能在已有个体上推导；改写时要么按等价规则重写公理，要么在语法层过滤、放弃这部分推理。能改写的部分（类层次、属性层次、域/值域、属性链等）进入规则引擎，这正是 OWL 2 RL 的思路。

Datalog 语法有三类成分：原子（atom）形如 p(x1, …, xn)，p 是谓词，括号里是项（变量或常量）；规则（rule）形如 H :- B1, …, Bm，H 是规则头（结论），B1…Bm 是规则体（前提合取），体中原子全成立则头成立；事实（fact）是体为空的规则，直接成立。重要约束安全规则：规则头中的每个变量都必须在体中出现，防止推出含无界变量的结论。规则可以递归，课件的路径例子即传递闭包：

path(X, Y) :- edge(X, Y).                       # 一条边本身是路径（事实性规则）
path(X, Y) :- path(X, Z), path(Z, Y).           # X 到 Z、Z 到 Y 都有路径，则 X 到 Y 有路径

前向推理（前向链接，forward chaining）从已知事实出发，反复用规则体匹配事实、把规则头作为新事实加入，直到不动点，即物化。

代表工具两款。KAON2 是 OWL 推理机与本体管理 API（Java），基于一阶消解把描述逻辑本体改写为 Datalog 再求值，针对大规模 ABox 优化，支持 OWL DL 与 SWRL。RDFox（牛津大学衍生企业 Oxford Semantic Technologies，由 Ian Horrocks、Boris Motik、Bernardo Cuenca Grau 于 2017 年创立）是内存 RDF 三元组存储，支持 Datalog 规则推理，主打并行化（多线程并行、更新时高效维护物化结果），支持 OWL 2 RL，C++ 内核、多语言接口。需要纠正一个常见误解：RDFox 不是开源软件，而是商业软件，运行须持有 license key，仅评估与学术用途免费授权；其母公司 Oxford Semantic Technologies 已于 2024 年 7 月被三星电子收购（三星 Galaxy S25 等的个人数据引擎即基于 RDFox 技术）。课件的 RDFox 实践用金融股权图谱，TBox 与 ABox 分开输入，命名空间 finance（http://www.example.org/kse/finance#），另手写两条业务规则：

finance:hold_share(X, Y) :- finance:control(X, Y).                  # 执掌一家公司就是其股东
finance:conn_trans(Y, Z) :- finance:hold_share(X, Y),               # 同一人持股的两家公司
                            finance:hold_share(X, Z), Y != Z.       # 存在关联交易；Y != Z 为课件规则之外补充的防自关联守卫

数据里孙宏斌执掌融创中国和乐视网、贾跃亭执掌乐视网；规则一推出 hold_share，规则二推出二者存在 conn_trans。RDFox 推理是”实例化 + 规则推理”结合：本体词汇（RL 部分）与自定义规则结论一起物化，新增事实时自动更新，对风控、舆情应用很有价值。常见疑问：为什么用自定义规则而不只用 OWL 公理？因为 OWL 只能用描述逻辑算子表达，业务逻辑（如关联交易）无法用类包含刻画，SWRL 则把 Horn 规则写进 OWL 本体。

4.3 基于一阶查询重写的方法：OBDA

第三类方法换了思路：不物化、不搬数据，查询时把本体查询”展开”成对底层数据源的查询，这套体系叫 OBDA（Ontology-Based Data Access，基于本体的数据访问），数据留在关系库、以查询语言为桥梁关联异构系统。中间语言是 Datalog——它既有一阶逻辑形式、又是数据库查询语言：SPARQL 先重写成 Datalog，再结合映射重写成 SQL。基本流程：用户只对本体层写 SPARQL；系统持有本体和一组”关系表到本体词汇”的映射（标准 R2RML）；查询先做查询重写（按公理展开成等价查询组），再做查询展开（本体词汇按映射替换成表的列），生成 SQL 交关系库执行，结果返回后结果转换回到本体层。数据留在原地、天然实时，适合大数据；代价是表达能力受限——只有能重写成一阶查询的部分（OWL 2 QL，即 DL-LiteR 片段）可用。这里要澄清：OWL 2 QL 本身就支持把右端（RHS）存在量词 ∃ 的包含公理在查询时重写展开（这正是 DL-Lite 查询重写的招牌能力，如 Researcher ⊑ ∃worksFor——研究者至少有一个任职机构，这类公理可在重写阶段并入查询，下文 q(x) ← worksFor(x, _) 这条重写用的正是它）；真正”造个体”无法查询时展开的，是需要引入底层数据库里根本不存在的新个体、或含合取/析取/基数约束等超出 DL-Lite 片段的公理。课件用科研管理例子演示三步重写：本体有 Researcher（研究人员）、Coordinator（协调专员，Researcher 子类）、Project（项目），底层是两张关系表 RESEARCHER(ID, name, project, type) 和 PROJECT(ID, name)，type 为 1 标记协调专员。用户的 SPARQL 是”查所有研究人员及其项目”：

PREFIX exp: <http://example.org/>
PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
SELECT ?r ?p
WHERE {
  ?r exp:worksFor ?p .
  ?p rdf:type exp:Project .
}

步骤一，按本体公理把查询重写成所有可能等价的 Datalog 查询（用不上的公理先在语法层过滤）：

q(x) ← worksFor(x, y), Project(y)
q(x) ← worksFor(x, y), worksFor(_, y)     # 有人共事的也是研究人员
q(x) ← worksFor(x, _)
q(x) ← Researcher(x)
q(x) ← Coordinator(x)

步骤二，把数据库关系映射成 Datalog 原子（下划线 _ 表示不关心的列）：

Researcher(x)  ← RESEARCHER(x, _, _, _)
Coordinator(x) ← RESEARCHER(x, _, _, 1)
Project(x)     ← PROJECT(x, _)
worksFor(x, y) ← RESEARCHER(x, _, y, _)
name(x, y)     ← RESEARCHER(x, y, _, _)
name(x, y)     ← PROJECT(x, y)

步骤三整合两组规则并逐层展开：“研究人员及其项目”展开为 q(x) ← RESEARCHER(x, _, y, _), PROJECT(y, _)，已是标准两表连接、易翻译成 SQL；“所有协调专员”展开为 q(x) ← RESEARCHER(x, _, _, 1)，退化为单表过滤。注意课件重写示例统一把目标写成一元 q(x)，只投影研究人员、项目变量仅用于连接，相对原 SPARQL 的 SELECT ?r ?p 是教学简化；要保留 ?p，把 q 写成二元 q(x, y) 即可。代表系统是 Ontop：开源 OBDA 系统（Apache License 2.0），兼容 RDFS、OWL 2 QL、R2RML、SPARQL 与主流关系库。下面代码对照”前向物化”与”查询时重写”：前者用 CONSTRUCT 多轮迭代把结论写回图，后者用属性路径在查询现场展开、原库不动；末尾演示递归规则 path 的不动点。

# -*- coding: utf-8 -*-
# 代码块4：前向链接"物化" vs 查询时"重写"——两种推理落地方式的最小对照
from rdflib import Graph, Namespace, RDF, RDFS

FIN = Namespace("http://www.example.org/kse/finance#")
g = Graph()
g.bind("fin", FIN)
g.parse(data="""
@prefix fin: <http://www.example.org/kse/finance#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
fin:地产公司 rdfs:subClassOf fin:公司 .
fin:公司 rdfs:subClassOf fin:法人实体 .
fin:融创中国 rdf:type fin:地产公司 .
""", format="turtle")

# 方式一：前向链接（materialization 物化）——把规则反复作用到知识库，直到不动点，结论写回库中
mat = Graph() + g
one_hop = """
PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
CONSTRUCT { ?x rdf:type ?sup }
WHERE { ?x rdf:type ?c . ?c rdfs:subClassOf ?sup . }"""
for _ in range(5):                       # 多轮应用规则，等价于 Datalog 的前向链接
    before = len(mat)
    mat += mat.query(one_hop).graph     # CONSTRUCT 返回的结论直接并回知识库
    if len(mat) == before:              # 没有新三元组，到达不动点
        break
print("物化：原库三元组", len(g), "-> 物化后", len(mat))

# 方式二：查询时重写（OBDA 思路）——原库一条三元组都不改，查询时用属性路径现场展开
q = """
PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
SELECT DISTINCT ?t WHERE { ?x rdf:type/rdfs:subClassOf* ?t . }"""
types = sorted(r.t.toPython().split("#")[-1]
               for r in g.query(q, initBindings={"x": FIN["融创中国"]}))
print("查询时重写：融创中国的类型", types, "；原库三元组仍为", len(g), "（数据不动）")

# Datalog 递归规则的集合语义：path(X,Y) :- edge(X,Y). path(X,Y) :- path(X,Z), path(Z,Y).
edge = {("a", "b"), ("b", "c"), ("c", "d")}
path = set(edge)
while True:
    new = {(x, z) for (x, y) in path for (y2, z) in path if y == y2}
    if new <= path:
        break
    path |= new
print("path 递归规则的不动点：", sorted(path))

4.4 基于产生式规则的方法

产生式系统（production system）是按机制执行规则达到目标的前向推理系统，与一阶逻辑相似但形式更自由，广泛用于自动规划与专家系统。它与知识图谱一脉相承：专家系统由推理引擎加规则库构成，图谱可视为专家系统在大数据时代的表现，也可直接充当知识库。

产生式系统由三部分组成。事实集合（Working Memory，WM）存放当前所有事实，事实称 WME：描述对象形如 (type attr1: val1 …)，如 (student name: Alice age: 24)；描述关系用具体化（Reification）写法，简记如 (olderThan John Alice)。产生式集合（Production Memory，PM）是规则集合，每条产生式形如 IF conditions THEN actions：conditions 称 LHS（条件部分），是条件的合取，全部满足时触发；actions 称 RHS（动作部分），是按序执行的动作序列。LHS 的 spec 可以是常量、变量、表达式（[n+4]）、布尔测试（{> 10}）及与或非组合；RHS 动作三种：ADD pattern 加事实、REMOVE i 移除匹配事实、MODIFY i 修改匹配事实属性。最简规则：IF (Student name: x) THEN ADD (Person name: x)。

推理引擎循环执行三个阶段：模式匹配——用每条规则的 LHS 匹配当前 WM，LHS 被满足的规则触发、进入议程（agenda）；解决冲突——同一时刻可能多条规则被触发，按策略从议程选一条，常见策略有随机、具体性（specificity，选条件最多的规则）、新近程度（recency，选最近没触发的规则）；纯推理动作只有 ADD、事实单调增长，一轮内全部执行与逐条执行结果相同，最小实现采用此简化；执行动作——执行 RHS 对 WM 增删改，WM 变化后回到匹配阶段，直到没有规则可触发。课件证券例子：红黄蓝事件的新闻被抽取为利空事件，触发止损规则 [SHORT] → [SELL]，SELL 带上股票代码、交易量等输入直接送交易系统，库中还有止盈、金叉买入等规则；若每轮拿每条规则扫全部事实，代价是规则数与事实数的乘积。RETE 算法解决此问题，1979 年由 Charles Forgy 在卡内基梅隆大学（CMU）提出，核心是把每条规则的 LHS 组织成判别网络、空间换时间：α 网络对每个单条件保存满足它的 WME 集合（事实增删时增量维护、不必重扫），β 网络保存条件间逐步连接（join）的中间结果，变量绑定沿网络汇合，完全匹配送入议程；事实只在变化时传播一次，结果可被多规则复用。

代表工具四款：Drools 是商用业务规则管理系统（BRMS），核心是 RETE 改进版（RETEOO / PHREAK），自带规则语言 DRL、可嵌入 Java；Jena 是语义网 Java 框架，提供 RDF/RDFS/OWL 接口、规则引擎与三元组存储查询；RDF4J（前身 Sesame）是开源 RDF 框架，支持解析、存储、推理、查询，用 SPARQL CONSTRUCT 表达规则；GraphDB（前身 OWLIM）基于 RDF4J，是含存储、推理、查询的语义存储系统，支持 RDFS、OWL DLP、OWL Horst、OWL 2 RL 等规则集。Drools 是通用规则管理系统，另外三款本质是图数据库/框架；原课还点出：Drools 只做自定义规则推理，RDFox 还做 OWL 2 RL 本体层实例化，推出的三元组更多。下面实现最小产生式系统：WM 带 α 索引、LHS 支持变量连接（β join）与内置不等测试，按具体性排序跑到不动点。

# -*- coding: utf-8 -*-
# 代码块5：最小产生式系统（事实集 WM + 产生式 PM + 推理引擎：匹配/冲突解决/执行）
from collections import defaultdict

def is_var(x):
    return isinstance(x, str) and x.startswith("?")

class WM:
    """事实集合（Working Memory）：事实为元组，如 ("type", "Alice", "TA")"""
    def __init__(self, facts):
        self.facts = list(facts)
        # α 网络雏形：按"谓词"为每个单条件建索引，匹配时只扫相关事实（空间换时间）
        self.alpha = defaultdict(list)
        for f in self.facts:
            self.alpha[f[0]].append(f)
    def add(self, wme):
        if wme not in self.facts:
            self.facts.append(wme)
            self.alpha[wme[0]].append(wme)
            return True
        return False

def match_one(fact, pattern):
    """单条件匹配：? 开头为变量，其余为常量；返回绑定或 None"""
    bind = {}
    for fv, pv in zip(fact, pattern):
        if is_var(pv):
            if pv in bind and bind[pv] != fv:
                return None
            bind[pv] = fv
        elif pv != fv:
            return None
    return bind

def join(binds1, binds2):
    """β 网络雏形：对两个条件的匹配结果按公共变量做连接"""
    out = []
    for b1 in binds1:
        for b2 in binds2:
            merged = dict(b1); ok = True
            for k, v in b2.items():
                if k in merged and merged[k] != v:
                    ok = False; break
                merged[k] = v
            if ok:
                out.append(merged)
    return out

class Rule:
    """产生式：lhs 为条件模式列表（条件之间是"且"），rhs 为动作列表；
    内置条件 ("NEQ", 变量1, 变量2) 表示两个变量必须取不同值"""
    def __init__(self, name, lhs, rhs):
        self.name, self.lhs, self.rhs = name, lhs, rhs

def match_rule(wm, rule):
    binds = [{}]
    for pat in rule.lhs:
        if pat[0] == "NEQ":           # 内置布尔测试，不匹配事实
            binds = [b for b in binds if b.get(pat[1]) != b.get(pat[2])]
            continue
        step = []
        for f in wm.alpha.get(pat[0], []):   # α 索引：只取该谓词下的事实
            b = match_one(f, pat)
            if b is not None:
                step.append(b)
        binds = join(binds, step)
        if not binds:
            return []
    return binds

def fire_once(wm, rules):
    """一轮推理：模式匹配 -> 议程 -> 冲突解决（specificity 排序）
    简化：纯推理动作只有 ADD（单调），一轮内按序执行议程中全部触发实例，
    与"每轮只选一条"的最终不动点相同"""
    agenda = []
    for rule in rules:
        for b in match_rule(wm, rule):
            agenda.append((rule, b))
    agenda.sort(key=lambda rb: len(rb[0].lhs), reverse=True)  # specificity：条件多者优先
    added = 0
    for rule, b in agenda:
        for kind, templ in rule.rhs:
            wme = tuple(b.get(x, x) if is_var(x) else x for x in templ)
            if kind == "ADD" and wm.add(wme):
                added += 1
                print(f"  规则[{rule.name}] 触发，ADD {wme}")
    return added

def run(wm, rules):
    """前向链接循环，直到没有新事实（不动点）"""
    rnd = 0
    while True:
        rnd += 1
        print(f"-- 第 {rnd} 轮 --")
        if fire_once(wm, rules) == 0:
            print("  无新事实，推理收敛")
            break

wm = WM([
    ("type", "Alice", "TA"), ("type", "Bob", "TA"), ("type", "Mary", "Student"),
    ("subClassOf", "TA", "Student"), ("subClassOf", "Student", "Person"),
    ("control", "孙宏斌", "融创中国"), ("control", "孙宏斌", "乐视网"),
    ("control", "贾跃亭", "乐视网"),
])
rules = [
    Rule("上下位补类型",
         [("type", "?x", "?y"), ("subClassOf", "?y", "?z")],
         [("ADD", ("type", "?x", "?z"))]),
    Rule("执掌即持股",
         [("control", "?x", "?y")],
         [("ADD", ("hold_share", "?x", "?y"))]),
    Rule("同控两家存关联交易",
         [("hold_share", "?x", "?y"), ("hold_share", "?x", "?z"), ("NEQ", "?y", "?z")],
         [("ADD", ("conn_trans", "?y", "?z"))]),
]
run(wm, rules)
print("最终事实条数:", len(wm.facts))

第一轮触发”执掌即持股”和一跳上下位补类型；第二轮”同控两家存关联交易”推出融创中国与乐视网的 conn_trans，类型链同时补到 Person；第三轮收敛。NEQ 守卫必不可少——否则 ?y 与 ?z 绑定同一家公司，会推出”公司与自己关联交易”的无意义结论，对应 Datalog 里常写的 Y != Z。四类方法定位对照见小结第 4 点。

五、Python 实操：金融图谱上的完整推理流水线

原课最后用 Jena 实践：Model 是 Jena 最核心的数据结构（即知识库），挂 RDFS 推理机得到 InfModel 做上下位推理，挂 OWL 推理机做类别补全，再调 validate 出不一致报告；本节用 rdflib 把这些机制复现一遍。数据沿用课件金融图谱：命名空间 finance，TBox 含类层次与不相交公理，ABox 含执掌关系与类型断言，并故意保留课件原例冲突——孙宏斌同时被声明为公司和人、人与公司不相交。

# -*- coding: utf-8 -*-
# 代码块6：金融图谱完整推理流水线（对应原课 Jena 实践：RDFS 推理机 / OWL 推理机 / validate）
from rdflib import Graph, Namespace, RDF, RDFS, OWL

FIN = Namespace("http://www.example.org/kse/finance#")
g = Graph()
g.bind("fin", FIN)
g.parse(data="""
@prefix fin: <http://www.example.org/kse/finance#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .

# ===== TBox（人工构建，规模通常不大）=====
fin:地产公司 rdfs:subClassOf fin:公司 .
fin:公司 rdfs:subClassOf fin:法人实体 .
fin:人 owl:disjointWith fin:公司 .
fin:control rdfs:domain fin:人 ; rdfs:range fin:公司 .

# ===== ABox（图谱事实）=====
fin:孙宏斌 fin:control fin:融创中国 , fin:乐视网 ;
           rdf:type fin:公司 , fin:人 .
fin:贾跃亭 fin:control fin:乐视网 .
fin:王健林 fin:control fin:万达集团 .
fin:融创中国 rdf:type fin:地产公司 .
""", format="turtle")

def local(t):
    return t.toPython().split("#")[-1]

# 1) 上下位推理（对应 Jena 的 createRDFSModel）：subClassOf 传递
print("== 1. 上下位推理：地产公司 的全部上位概念 ==")
q_super = """
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
SELECT ?t WHERE { ?c rdfs:subClassOf+ ?t . }"""
for row in g.query(q_super, initBindings={"c": FIN["地产公司"]}):
    print("   地产公司 ⊑", local(row.t))

# 2) 类别补全（对应 OWL 推理机的 printStatements(x, RDF.type, null)）
print("== 2. 类别补全：融创中国 的全部类型 ==")
q_type = """
PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
SELECT DISTINCT ?t WHERE { ?x rdf:type/rdfs:subClassOf* ?t . }"""
for row in g.query(q_type, initBindings={"x": FIN["融创中国"]}):
    print("   融创中国 rdf:type", local(row.t))

# 3) 自定义规则（对应 RDFox/Drools 的两条 Datalog 规则）
print("== 3. 规则推理：执掌->持股；同一人持股的两家不同公司->关联交易 ==")
hold = set(g.subject_objects(FIN.control))             # hold_share(X,Y) :- control(X,Y)
for x, y in sorted(hold, key=str):
    print(f"   hold_share({local(x)}, {local(y)})")
conn = set()
for x, y in hold:                                      # conn_trans(Y,Z) :- hold_share(X,Y), hold_share(X,Z)（课件原规则；此处补 Y!=Z 防自关联）
    for x2, z in hold:
        if x == x2 and y != z:
            conn.add((y, z))
for y, z in sorted(conn, key=str):
    print(f"   conn_trans({local(y)}, {local(z)})")

# 4) 不一致检测（对应 InfModel.validate()）：检查 disjointWith 冲突并给出辩解
print("== 4. 不一致检测 ==")
disjoint = {}
for a, b in g.subject_objects(OWL.disjointWith):
    disjoint.setdefault(a, set()).add(b)
types = {}
for s, o in g.subject_objects(RDF.type):
    types.setdefault(s, set()).add(o)
n_bad = 0
for inst, cs in types.items():
    for c in cs:
        for d in disjoint.get(c, ()):
            if d in cs:
                n_bad += 1
                print(f"   冲突：{local(inst)} 同时是 {local(c)} 和 {local(d)}，二者 owl:disjointWith")
                print(f"   辩解：{local(inst)} rdf:type {local(c)}；{local(inst)} rdf:type {local(d)}；"
                      f"{local(c)} owl:disjointWith {local(d)}")
print("   不一致条数：", n_bad)

对照 Jena 接口：第一步上下位推理对应 createRDFSModel（沿 subClassOf 链推导、查询触发）；第二步类别补全对应 InfModel 挂 OWL 推理机打印个体全部 rdf:type；第三步自定义规则对应 RDFox/Drools 的两条 Datalog 规则；第四步不一致检测对应 validate() 返回的 ValidityReport——课件原例报告的正是”孙宏斌 type 公司、孙宏斌 type 人”与”人 disjointWith 公司”不兼容；这类检测在 Jena 中必须挂 OWL 推理机（RDFS 推理机不认识 disjointWith），下面的 rdflib 复现改为手工遍历 owl:disjointWith 与 rdf:type 三元组达到同样效果。重型框架的推理机并不神秘，只是把闭包计算、规则匹配、冲突校验工程化、增量化；用 Python 复现核心推理只需几十行。

📝 动手练一练

练习 1（概念辨析，口头作答）：没有孩子的人是否属于 ∀hasChild.Doctor？是否属于 ∃hasChild.Doctor？用 1.3 节集合语义说明。

练习 2（代码）：在 rdflib 中实现 owl:inverseOf（P(s,o) 推出 Q(o,s)）与 rdfs:domain / rdfs:range（P(s,o) 推出 s type D、o type R）。数据：hasChild inverseOf hasParent，domain 为 Parent、range 为 Child，已知 Alice hasChild Bob，验证能否推出 Bob hasParent Alice、Alice 是 Parent、Bob 是 Child。

# -*- coding: utf-8 -*-
# 练习参考答案：inverseOf 互逆推理 + domain/range 补类型
from rdflib import Graph, Namespace, RDF, RDFS, OWL

FAM = Namespace("http://example.org/fam#")
g = Graph()
g.bind("fam", FAM)
g.parse(data="""
@prefix fam: <http://example.org/fam#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .

fam:hasChild owl:inverseOf fam:hasParent .
fam:hasChild rdfs:domain fam:Parent ; rdfs:range fam:Child .
fam:Alice fam:hasChild fam:Bob .
""", format="turtle")

def local(t):
    return t.toPython().split("#")[-1]

inferred = Graph()  # 存放推理结论，与原始事实分开便于观察

# 规则一：owl:inverseOf —— P owl:inverseOf Q 且 P(s,o)，则 Q(o,s)
for p, q in g.subject_objects(OWL.inverseOf):
    for s, o in g.subject_objects(p):
        inferred.add((o, q, s))
        print(f"inverseOf：{local(o)} {local(q)} {local(s)}  <- {local(s)} {local(p)} {local(o)}")

# 规则二：rdfs:domain —— P rdfs:domain D 且 P(s,o)，则 s rdf:type D
# 规则三：rdfs:range  —— P rdfs:range  R 且 P(s,o)，则 o rdf:type R
for p, d in g.subject_objects(RDFS.domain):
    for s, o in g.subject_objects(p):
        inferred.add((s, RDF.type, d))
        print(f"domain：{local(s)} rdf:type {local(d)}")
for p, r in g.subject_objects(RDFS.range):
    for s, o in g.subject_objects(p):
        inferred.add((o, RDF.type, r))
        print(f"range：{local(o)} rdf:type {local(r)}")

print("推出的新三元组条数：", len(inferred))

练习 3（机制简答）：规则 type(x,y)、subClassOf(y,z) ⇒ ADD type(x,z) 在 RETE 网络中如何流动？α 网络和 β 网络分别保存什么？

本章小结

本节沿”为什么能推理—推理做什么—怎么推理—怎么落地”展开：

1. OWL 以描述逻辑为内核，描述逻辑是一阶谓词逻辑的可判定子集；知识库 K=(T,A)，TBox 是概念与关系的公理集（类比 schema），ABox 是个体断言集（类比 data）。
2. 形式语义由”解释 I=(Δ^I, ·^I)“给出：概念解释成论域子集、关系解释成二元组集合，⊓/⊔/¬/∃/∀ 分别对应交集、并集、补集和两种量词集合；模型、可满足、逻辑蕴含都建立在解释之上，推理因此有正确性与完备性双重保证。
3. 四大标准任务：可满足性（有没有模型）、分类（TBox 算概念包含）、实例化（ABox 算新实例与新关系，即物化）、不一致性检测（disjointness 冲突）；辩解是课件标注的非标准推理，给出结论的最小前提公理集，用于调试。
4. 四类方法各有定位：Tableaux 用扩展规则不断扩充 ABox（严格说是完成树）、检查是否出现矛盾（clash），出现矛盾就回溯分支——可借”反证法/试探能否构造出模型”来理解，但严格讲它走的是完成树加阻塞，并非归结反驳（FaCT++/Racer/Pellet/HermiT）；Datalog 改写把公理变成规则（KAON2 基于一阶消解、支持 OWL DL/SWRL，RDFox 面向 OWL 2 RL 做并行前向物化）；查询重写走 OBDA、SPARQL 经 Datalog 重写成 SQL（Ontop，对应 OWL 2 QL）；产生式系统按”匹配—冲突解决—执行”循环，RETE 用 α/β 判别网络空间换时间（Drools/Jena/RDF4J 为 RETE 系，GraphDB 用自研 TRREE 引擎）。
5. 工程上，上下位推理、类别补全、自定义规则、不一致检测都能用 rdflib 在几十行内复现，重型框架只是把这些机制工程化、增量化。

📋 行动清单

• 讲清 TBox 与 ABox 的区别，各写出 3 条公理/断言例子（对照 schema 与 data）
• 默写 ⊓、⊔、¬、∃、∀ 五个算子的集合语义，解释空真现象
• 区分正确性（soundness）与完备性（completeness），说明链路预测为什么给不出这两个保证
• 把四大标准任务与辩解各对应到一个具体例子（Apple/选股/Mother/心内膜炎/脑膜炎）
• 手推 Allen 例子的 Tableaux 过程（⊓− → ⊑ → ⊥），说明”待反驳结论本就在本体中”意味着什么
• 写出一条安全的 Datalog 规则，解释规则推理为什么处理不了 ∃ 和 ¬
• 口述 OBDA 三步重写流程（SPARQL→Datalog→SQL），说出它相对物化的优点与表达能力限制
• 画出产生式系统”WM/PM/推理引擎”三部分与”匹配—冲突解决—执行”循环，解释 RETE 的 α/β 网络各存什么
• 跑通代码块6 的金融图谱流水线，并把练习2 的 inverseOf/domain/range 规则合并进去
• 遇到推理机报错或错误结论时，用”辩解”思路定位最小公理集，而不是直接删掉结论

—— 小象教研组