This paper encodes more than 600 Event-B proof rules in Prolog and integrates them into ProB, producing an interactive sequent prover with proof-tree visualisation. The system imports proof obligations from the Rodin platform and exports ProB replay traces, tool-independent interactive HTML proof trees, and results back to Rodin. Compared with an earlier Java implementation, the Prolog version is described as more compact, maintainable, and extensible. A preliminary iterative-deepening prover with simple heuristics can already find short proofs, while faster automated provers remain future work.
No heat snapshots are available in the last 24 hours.