用 Prolog 编码 Event-B 证明规则：面向 ProB 的交互式序列演算证明器

论文将超过600条 Event-B 证明规则编码为 Prolog，并集成进基于 Prolog 的 ProB 验证工具，形成支持证明树可视化的交互式序列演算系统。工具可导入 Rodin 证明义务，导出 ProB 重放轨迹、独立 HTML 证明树及 Rodin 结果；初步迭代加深证明器已能寻找短证明。