AYXK 本体说明 全局 结构 桥接校验
ayxk-v1.owl · AST 读法

本体写成一棵语法树

像看代码的 AST：根是「整份菜谱」，枝是种类 / 连线 / 规矩。下面再用同一棵树的形状，拆开刚才 HermiT 实际推出的三步。

绿字＝操作 / 节点种类 青字＝关键字 黄字＝具体名字

1. 本体里都写了什么（整棵 AST）

文件 ayxk-v1.owl。三块：种类树、连线规矩、几条硬公理。预留种类（人/机构…）在树上，库里还没启用。

  • Ontology 遨游星空 v1
    • Classes 种类 = 抽屉标签
      • Entity 实体 · 根
        • Person 人 · 预留
        • Org 机构 · 预留
        • Place 地点 · 预留
        • Topic 主题 · 已启用
        • Artifact / WebPage / Event / Note / Project / Source 预留；网页⊑制品
        • DecisionNode 决策零件父类
          • Decision
            • DecidedDecision
              • ⊑ Decision
              • ≥1 chooses 至少选一条路
          • Goal 问题
          • Constraint 硬条件
          • Risk
          • Option
          • Evidence
          • Outcome
    • ObjectProperties 连线 = 谁→谁
      • asks : Decision → Goal
      • constrained_by : Decision → Constraint
      • considers : Decision → Option
        • chooses ⊑ considers 选择
        • rejects ⊑ considers 拒绝
      • because : Decision → Evidence
      • supported_by : Option → Evidence
      • opposed_by : Decision|Option → Risk|Evidence
      • about : Entity → Topic
      • supersedes : Decision → Decision
      • 计划边 related_to / involves / supports / part_of / hasSource
    • DataProperties 字段
      • title / body / nodeId / status / edgeNote
    • Axioms 硬规矩
      • Disjoint Decision · Goal · Constraint · Risk · Option · Evidence · Outcome
      • SubProperty chooses ⊑ considers · rejects ⊑ considers
      • Restriction DecidedDecision ⇒ ≥1 chooses
      • Bridge 不许孤立节点（闭世界 · 不在 OWL）

2. 推理①：收标签（归类简化）

对「AYXK 主存储选型」：手写贴了 Decision + DecidedDecision。HermiT 用子类公理收成只要 DecidedDecision。

  • 事实 主存储选型
    • rdf:type Decision
    • rdf:type DecidedDecision
  • 公理
    • DecidedDecision ⊑ Decision
  • Derive 推理结果
    • 主存储选型
      • rdf:type DecidedDecision 够用
      • Decision 标签可省略（已蕴含）

3. 推理②：亲属关系（属性层级）

菜谱写 chooses / rejects 都是 considers 的孩子。推理机确认家谱；开放世界下不一定把实例上的「考虑过」列表自动填满。

  • PropertyHierarchy
    • considers 考虑过
      • chooses ⊑ considers
        • 实例 选型 chooses SQLite…
      • rejects ⊑ considers
        • 实例 选型 rejects CMS
        • 实例 选型 rejects 手搓页
    • Derive chooses、rejects 的父属性 = considers

4. 推理③：打架（互斥）

故意加一句：主存储选型 也是 Goal。和 Disjoint 公理冲突 → HermiT 拒绝整棵树。

  • 公理 AllDisjointClasses
    • Decision · Goal · Option · …
  • 事实 主存储选型
    • type Decision（已有）
    • type Goal（故意加的）
  • Derive InconsistentOntology
    • 不能同时属于两个互斥抽屉

5. 为什么「缺 chooses」推理机不骂？

开放世界：没写≠没有。缺边要靠桥接清单抓。

  • HermiT
    • 输入：菜谱+部分事实
    • 输出：归类 / 层级 / 互斥警报
    • 缺边 → 常当「未知」
  • 桥接校验
    • 输入：SQLite 全表
    • 输出：漏写 / 连错类型
    • 已拍板必须有 chooses → 会打叉

权威 OWL：protege-lab/ontologies/ayxk-v1.owl · 推理演示：ontology/run_reason_demo.py · 白话本体页 · 桥接校验