Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB

Abstract: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.

In Proceedings ICLP 2026, arXiv:2607.17707

Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Software Engineering (cs.SE)

arXiv:2607.21191 [cs.LO]

(or arXiv:2607.21191v1 [cs.LO] for this version)

https://doi.org/10.48550/arXiv.2607.21191 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

EPTCS 450, 2026, pp. 134-147

https://doi.org/10.4204/EPTCS.450.12 Focus to learn more DOI(s) linking to related resources

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.