Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper details the encoding of over 600 Event-B proof rules in Prolog, facilitating a more systematic and interactive proof analysis through the ProB validation tool. The integration allows for proof tree visualization and enhances the educational experience by giving students direct control over proof rule selection. Compared to the prior Java implementation, the Prolog encoding is found to be more compact, maintainable, and extensible, paving the way for future developments in automatic provers.
Encoding Event-B proof rules in Prolog not only streamlines proof analysis but also transforms how students engage with formal methods through interactive visualization.
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.