用Prolog实现600多条事件逻辑证明规则，支持交互式推理与可视化。
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
- 将600+条事件逻辑证明规则编码为Prolog规则，实现系统化推导
- 支持从Rodin导入证明任务，可生成可回放的证明轨迹和网页版证明树
- 适合形式化方法教学与验证工具链集成，代码更易维护扩展
事件逻辑是一种基于谓词逻辑和集合论的形式化方法。本文将超过600条证明规则用Prolog实现，支持系统化、可理解的证明分析与构建。通过集成到基于Prolog的验证工具ProB中，实现了具备证明树可视化的交互式证明系统，有助于学生直接控制证明规则的选择。该工具可从Rodin平台导入证明需求，支持多种输出：用于ProB中回放的轨迹文件、无需依赖工具的交互式HTML证明树文档，以及可导回Rodin的证明结果，使ProB可作为第二验证链使用。相较于此前用Java实现的版本，Prolog编码更紧凑、易维护且易扩展。目前已有基于迭代加深搜索与简单启发式策略的初步自动证明器，已可用于快速寻找短证明，未来目标是开发高效自动证明器。
原文摘要 · Abstract (English)
Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system with proof tree visualisation. This has advantages in teaching, giving students direct control over the selection of proof rules. Our tool can import proof obligations from the Rodin platform and provides multiple exports: a trace file for proof replay in ProB, an interactive HTML document for tool-independent exploration of the proof tree, and an export back to Rodin, allowing the ProB prover to be used as second chain. Compared to the previous implementation of the proof rules in Java, the encoding in Prolog is more compact, maintainable and extensible. While a preliminary iterative deepening prover with simple heuristics is already available and useful for finding short proofs, we aim to obtain fast automatic provers in the future.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。