发表机构
Faculty of Mathematics; Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universit\" a tsstr. 1, D-40225 D\" u sseldorf（; ）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究将600多条Event-B证明规则编码到Prolog，集成到ProB工具形成交互式证明系统，有证明树可视化等优势，可导入导出，相比Java编码更优，未来目标是获得快速自动证明器。
AI 中文摘要
Event-B是一种基于谓词逻辑和集合论的形式化方法。我们在Prolog中编码了600多条证明规则，实现了系统且可理解的证明分析与构建。通过将证明规则集成到基于Prolog的验证工具ProB中，得到了一个带有证明树可视化的交互式证明系统。这在教学方面具有优势，能让学生直接控制证明规则的选择。我们的工具可从Rodin平台导入证明义务并提供多种导出方式。与之前用Java实现的证明规则相比，Prolog编码更紧凑、可维护且可扩展。虽然已有初步的带简单启发式的迭代加深证明器可用于找到简短证明，但我们未来旨在获得快速自动证明器。
英文摘要
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.
CommentsIn Proceedings ICLP 2026, arXiv:2607.17707
Journal refEPTCS 450, 2026, pp. 134-147
