Paper deep dive

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

Katharina Engels, Jan Gruteser, Michael Leuschel

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 48

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%

Last extracted: 7/24/2026, 2:46:43 AM

Summary

The paper presents an interactive sequent prover for the Event-B formal method, implemented in Prolog and integrated into the ProB tool. It encodes over 600 proof rules, enabling step-by-step proof construction, visualization, and export capabilities, offering advantages in teaching and maintainability compared to previous Java-based implementations in the Rodin platform.

Entities (8)

Event-B · formal-method · 98%ProB · software-tool · 97%Prolog · programming-language · 96%Rodin · software-platform · 95%Proof Rules · concept · 92%Proof Obligations · concept · 90%Java · programming-language · 85%Z3 · software-tool · 80%

Relation Signals (6)

ProB → implements → Event-B Proof Rules

confidence 95% · By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system

Prolog → usedfor → Encoding Proof Rules

confidence 94% · We encoded over 600 proof rules in Prolog

ProB → supports → Interactive Visualization

confidence 92% · we obtain an interactive proof system with proof tree visualisation

ProB → integrateswith → Rodin

confidence 90% · Our tool can import proof obligations from the Rodin platform... export back to Rodin

Prolog → comparedto → Java

confidence 88% · Compared to the previous implementation of the proof rules in Java, the encoding in Prolog is more compact

ProB → interfaceswith → Z3

confidence 85% · interface to external provers, such as SMT solvers, namely Z3

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

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.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

46,685 characters extracted from source content.

Expand or collapse full text

W. Faber, L. Giordano, R. Rocha, V. Santos Costa (Eds.): 42nd International Conference on Logic Programming (ICLP 2026) EPTCS 450, 2026, p. 134–147, doi:10.4204/EPTCS.450.12 © K. Engels, J. Gruteser, and M. Leuschel This work is licensed under the Creative Commons Attribution License. Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for PROB Katharina Engels Jan GruteserMichael Leuschel Faculty of Mathematics and Natural Science, Institute of Computer Science, Heinrich Heine University D ̈ usseldorf, Universit ̈ atsstr. 1, D-40225 D ̈ usseldorf katharina.engels,jan.gruteser,michael.leuschel@hhu.de 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 RODINplatform 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. 1 Introduction and Motivation In this work, we have developed a new interactive and automated theorem prover in Prolog for the Event- B formal method. The Event-B language introduced by Abrial [1, 2] is founded on predicate logic and set theory and builds on invariants and refinement to develop systems that are correct by construction, where proving is a crucial part to mathematically verify the system’s correctness. The logic of Event-B is underpinned by over 600 proof rules in sequent calculus style [12]. These proof rules are embedded in the RODINplatform [3], which also caters for several industrial and academic plugins to automatically conduct proofs. The RODINplatform contains the proof obligation generator, which generates proof obligations (POs) for an Event-B model. Discharging all POs ensures consistency and correctness of the model. Rodin POs as Prolog Facts .pl Proof Rules in Prolog Proof .bpr Trace .html ProBAnimator State Visualisation Export POs forProB Load via XTL Interface manual/ autom. Replay Replay Figure 1: Architecture of PROB’s Sequent Prover The initial motivation of this work came from teaching. While the Event- B proof rules are discussed in detail during lectures and are presented in the literature [2], RODINoften applies sev- eral proof steps simultaneously. The plugins of RODINalso conduct an en- tire proof in a single step.In both cases, the user or student cannot easily check, understand or reproduce a proof. Hence, the initial intention was to de- velop an interactive prover for Event-B, enabling students to apply or replay proof rules step by step and gain experience through experimentation. Our implementation, however, has a variety of other benefits K. Engels, J. Gruteser, and M. Leuschel135 for advanced users: a second independent toolchain to double-check proofs, new visualisation and anal- ysis features, and a new automatic prover producing proofs that are more robust to model changes and easier to reproduce upon changes of the proof itself. In this article, we show how the mathematical definitions of Event-B can be turned into executable Prolog rules that are still close to the original definition and can be used for proving. This includes almost all of RODIN’s inference and rewrite rules 1 , but also a few additional rules proposed by Abrial [2]. Within the RODINplatform, the rules are implemented in Java. By re-implementing those proof rules in Prolog, we have obtained a more compact code base. The encoding in Prolog is easier to maintain, extend for new proof rules and can be used for more purposes than the original Java code. In particular, we can use Prolog’s search capabilities for automatically generating proofs. With the PROB validation tool [25, 24] written in Prolog (cf. Figure 1), we can bring the proof rules to life and turn them into a labelled transition system, where the sequents are the states and each application of a proof rule is a transition. This allows students and regular users to choose which proof rule is applied at each proof step but also enables interactive HTML visualisations of finished proofs. By generating RODINproof files (BPR) in XML format, we close the loop to the RODINprover, enabling the PROB sequent prover to be used as a second chain. In this article, we present the following core contributions: • a Prolog implementation of Event-B proof inference and rewrite rules, • a comparison of the existing Java code in the RODINtool with our Prolog code regarding the code size and the effort required to implement a new rule, • the integration of the proof rules into the validation tool PROB, featuring –an interactive sequent prover using the PROB animator, along with an interactive visualisa- tion showing the current proof sequent, –an export of a proof tree visualisation as interactive HTML document using PROB’s interface to Graphviz for detailed analysis and teaching, –an export of a proof as BPR file for replay in the RODINplatform, • a first version of an automated prover for later integration in RODIN, and • a demonstration of the usefulness of the tooling for teaching proofs and logics in the context of formal modelling. 2 Event-B Proofs In Event-B, proof obligations (POs) must be proven to verify the correctness of a model. Proof obliga- tions arise, for example, from invariants, refinement, user-specified theorems or well-definedness condi- tions such as potential divisions by zero. 2 Depending on the type of a PO, a selection of hypothesesHis available to prove the goalG. Formally, a PO can be represented by a sequentH⊢G. This sequent expresses that the goalGlogically follows from the set of hypothesesHusing the proof rules of Event-B. 1 https://wiki.event-b.org/index.php/Inference Rules/AllRewriteRules 2 In the case of a PO for invariant preservation for some event, the hypotheses include defined axioms, theorems and the invariants applied to the state variables before the event. 136Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover forPROB One can use a set of different inference rules to prove a sequent. One of these rules is theHYP rule (H,P⊢P), which states that a sequent is proven if the goal is contained in the hypotheses. Two other inference rules are depicted below: ANDR H⊢PH⊢Q H⊢P∧QH,f∈E→F⊢f∈Type E 7→Type F FUN GOAL The left rule states that if the goal is a conjunction, the sequent can be proven by showing that each conjunct follows from the hypotheses individually. The right rule states thatfis a partial function (7→ symbol) if it is a total function(→symbol) for some domainEand rangeF. We use an example PO from an Event-B mars rover model 3 that will be used throughout the next chapters. A safety invariant states that the rover must not be exposed to excessive radiation, expressed byradiation(rover)≤α max , whereradiationassigns a radiation value to a position. For this in- variant, a well-definedness (WD) PO is created, as function application is only defined ifradiationis actually a function androveris in the domain ofradiation. A complete proof of the WD PO is de- picted in Figure 2. For brevity, we omit hypotheses that are not relevant for the proof. Starting from the original goal on the left of Figure 2, the conjunction is split into two subgoals by applying theAND Rrule. To discharge the first resulting sequent at the top, we apply theFUNGOALrule following from the first hy- pothesis. For the next sequent, we apply a rule for total relations and functions (DERIV DOMTOTALREL) to remove the domain operatordomfrom the goal. The second hypothesis contains a singleton set and can be simplified using theSIMPSUBSETEQSINGrule, after which we can discharge the goal by using theHYPrule. radiation∈field→N rover⊆field ⊢ radiation∈Z×Z7→Z ∧rover∈dom(radiation) radiation∈field→N rover⊆field ⊢ radiation∈Z×Z7→Z ∈Z×Z7→Z ∈Z×Z7→Z Proven radiation∈field→N rover⊆field ⊢ rover∈ ∈ ∈dom(radiation) radiation∈field→N rover⊆field ⊢ rover∈ ∈ ∈field radiation∈field→N rover∈ ∈ ∈field ⊢ rover∈field Proven ANDR FUNGOAL DERIVDOM TOTALREL SIMPSUB- SETEQSING HYP Figure 2: Application of Inference and Rewrite Rules to Prove a PO 3 State-Based Representation of Proof Obligations PROB [24] is an animator and model checker for high-level formal models. It contains a constraint solver and interpreter for B and Event-B. The XTL mode of PROB [16] allows one to circumvent the interpreter and directly load and then animate Prolog files that specify labelled transition systems. 4 The Prolog files define the ternary transition predicatetrans(Label,StateBefore,StateAfter), where the states of a transition system are represented as Prolog terms. The initial states are provided using thestart(State)predicate. State properties can be specified withprop(State,Property). Here, we use them for better comprehensibility only. In the following, we use PROB’s XTL mode to turn the Event-B proof rules into an animatable transition system. 3 Available at https://stups.hhu-hosting.de/models/sequentprover. 4 Detailed documentation at: https://prob.hhu.de/w/index.php?title=Other languages. K. Engels, J. Gruteser, and M. Leuschel137 Listing 1: Simple XTL Specification of a Button start(button(on)). trans(toggle_button,button(X),button(Y)) :- toggle(X,Y). prop(button(X),'='(button,X)). toggle(on,off). toggle(off,on). The code in Listing 1 demonstrates the XTL functionality for a simple button. Ini- tially, the button isonand can be toggled to the other state via a transition. The property shows the current state of the button. For our sequent prover, the state repre- sentation is slightly more complex. An example is shown in Listing 2, illustrating the Prolog rep- resentation of the start state for the PO discussed in Section 2. In general, a state has the form state(sequent(SelHyps,Goal,Cont),Info). The list of selected hypotheses is kept in the first entrySelHyps; the currentGoalis the second entry. 5 Only selected hypotheses are visible for proof rules; these can always be deselected and vice versa to hide those that are not required for a particular proof. ThecontinuationContis eithersuccessor is the next still unproven sequent (which has another continuation itself). In the initial state, there is exactly one open goal, so the continuation issuccess. If the current state becomessuccess, then the proof has succeeded and there are no more open goals to show. TheInfofield attached to the state is a list of additional information, including the deselected hypotheses and details about enumerated or deferred sets for typing. Listing 2: PO proven in Figure 2 represented as State Term start(state(sequent( [member('$'(radiation), total_function('$'(field),'NATURAL')), subset(set_extension(['$'(rover)]),'$'(field))], conjunct(member('$'(radiation), partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')), member('$'(rover),domain('$'(radiation)))), success),Info),[description(Label)]). Since PROB is not yet capable ofgeneratingproof obligations (POs) 6 , we use the RODINplatform for generation of POs for Event-B specifications. Using the PROB RODIN-Plugin, the generated POs can be exported as one file containing all obligations related to the selected machine (or context) as Prolog facts of the formdisprover_po(Label,Context,Goal,AllHyps,SelHyps,Status). This format was originally designed for the PROB Disprover [20]. Hence, we can easily reuse it to load and convert the POs for our sequent prover within PROB. The first entry is the label of the PO, which distinguishes POs according to a systematic naming scheme. For invariants, it consists of the event name, the label given to the invariant and the category of the PO (event/invariantlabel/INV). TheGoalis represented as anuntypedabstract syntax tree (AST) as are all available hypotheses inAllHypsand pre-selected ones inSelHyps.Statuscontains the RODINproof status. TheContextis used to extract user-defined types (Event-B sets), which are required for certain type rewriting rules. The Prolog representation of the goal and the hypotheses is normalised according to PROB’s WD prover [22]. Using the same format as the WD prover facilitates the integration of the proof rules into the PROB core. Then, the normalised hypotheses are combined with the goal into a term that represents the initialstateof the PO as shown in Listing 2. Finally, all POs of a machine are made available as initial states together with their corresponding labelstart(InitState,[description(Label)]), where the optional second argument is for the transition property explained in the following section. 5 Formulas are represented as a normalised abstract syntax tree. The term ‘$’ denotes an identifier. 6 The WD prover can already compute WD conditions, which we utilise later in this article. 138Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover forPROB 4 Proof Rules as a Transition System To define how proof rules transform a sequent into another or more successor sequents, the transi- tion predicate that was introduced in the previous section can be used. Take for example the rule SIMPSUBSETEQSINGwe applied in Section 2. It encodesE⊆S≡E∈S, which we can implement in Prolog and XTL as shown in Listing 3. 7 The first two clauses group together several simplification Listing 3: Implementation of Simplification and Rewrite Rules trans(simplify_goal(RuleName),state(sequent(Hyps,OldGoal,Cont),Info), state(sequent(Hyps,NewGoal,Cont),Info)) :- simp_rule(OldGoal,NewGoal,RuleName,Hyps). trans(simplify_hyp(RuleName),state(sequent(OldHyps,Goal,Cont),Info), state(sequent(NewHyps,Goal,Cont),Info)) :- select(Hyp,OldHyps,NewHyp,NewHyps), simp_rule(Hyp,NewHyp,RuleName,OldHyps). ... simp_rule(subset(SetA,S),member(A,S),'SIMP_SUBSETEQ_SING',_) :- singleton_set(SetA,A). simp_rule(not_equal(L,L),falsity,'SIMP_MULTI_NOTEQUAL',_). rules, which we apply either to the goal or to a specific hypothesis. That is, there are many other clauses forsimprule, two of which we show in Listing 3. This separation allows us to express a formal rule intuitively as one Prolog clause, with the original formula as the first argument, the rewritten formula as the second argument, and additional side conditions forming the body. In Listing 4, we show a selection of other rules. Listing 4: Prolog Rules Used for the Proof in Figure 2 simp_rule(domain(R),Dom,'DERIV_DOM_TOTALREL',Hyps) :- member(member(R,RType),Hyps), is_rel(RType,total,Dom,_). is_rel(total_relation(Dom,Ran),total,Dom,Ran). ... trans(and_r,state(sequent(Hyps,conjunct(G1,G2),Cont),I), state(NewSequent,I)) :- op_to_list(conjunct(G1,G2),ListOfConjuncts,conjunct), add_goals(Hyps,ListOfConjuncts,Cont,NewSequent). trans(Rule,state(sequent(Hyps,Goal,Cont),I),state(Cont,I)) :- axiom(Rule,Hyps,Goal). trans(Rule,state(sequent(Hyps,Goal,Cont),I),state(Cont,I)) :- axiom_with_info(Rule,Hyps,Goal,I). ... axiom(hyp,Hyps,Goal) :- member_hyps(Goal,Hyps). ... axiom_with_info(fun_goal,Hyps,member(F,partial_function(Ty1,Ty2)),Info) :- type_expression(Ty1,Info), type_expression(Ty2,Info), member(member(F,FType),Hyps), is_fun(FType,_,_,_). • For example, there are more complicated simplification rules likeDERIVDOMTOTALREL, where the rule needs access to all hypotheses. Note that inmember(member(R,RType),Hyps), the inner memberrepresents the AST node of the membership operator and the outer one checks for Prolog list membership. 7 We make minor modifications of the source code here to ease understanding. K. Engels, J. Gruteser, and M. Leuschel139 • We show the encoding of theANDRrule, which decomposes the goalconjunct(G1,G2)into its conjuncts. The current goal is replaced with the leftmost conjunct and the other conjuncts are added to the continuation (this is done byaddgoalsin line 8 of Listing 4). • We haveaxiomsas terminal proof steps, which close a proof branch without generating successor sequents, e.g.HYPandFUN GOAL. HYPis applied whenever the current goal is already contained in the hypotheses, i.e., when unifi- cation succeeds. One must consider that Prolog unification is insufficient for associative-commutative operations to determine equality [26]. Expressions such asadd(add(x,y),z)andadd(x,add(y,z)) oradd(add(z,y),x)cannot be unified directly. Instead, inmemberhypsground terms are then nor- malised into special lists to remove nesting, and compared by sorting. Moreover, it is taken into account that hypotheses may be stronger than the goal. For example,HYPcan be applied fory<x⊢x≥y. The applicability offun goaldepends on the goal having a particular form.typeexpression facts accept base types in the first argument directly, whereas composite type expressions are validated recursively. The second argument (Info) is used to look up custom data types in the list of meta- information. To make type information available, including user-introduced types, the hypotheses are type-checked at the beginning of the proof and the resulting information is stored inInfo. Rewrite rules can be applied to both top-level expressions and subterms by recursively descending into the structure of a term and attempting to apply a simplification rule to its arguments. That is why domain('$'(radiation))inmember('$'(rover),domain('$'(radiation)))can be simplified to'$'(field)(recall Figure 2). When applying particular rules, new identifiers need to be introduced, for instance, when rewriting S̸=∅to∃x·x∈Swith a fresh identifierx. To achieve this, a list of existing identifiers in an expression is computed, and a new identifier is generated that does not appear in that list. Transition Descriptions.PROB allows to adddynamictransition properties depending on the param- eter values and the state in which the transition is available. In our case, we use this feature to add user-friendly transition descriptions by adding a propertydescription/1. These are used to display the transition descriptions in PROB2-UI or in the HTML exports (see, e.g., Figures 4 and 5). Rules with User Input.Certain inference rules require user input, such as when adding new hypothe- ses or instantiating free identifiers of a universally quantified variable: FORALL INST H⊢WD(E)H,[x:=E]P⊢G H,∀x·P⊢G For this, we usesymbolictransitions specified by the predicatesymbtrans/3in a similar way as fortrans/3. However, symbolic transitions are not automatically evaluated during animation and can only be invoked manually. In the case of a universal quantifier, the user must provide the index of the universally quantified hypothesis to be instantiated, as well as a B expressionEfor the instantiation. In addition,Emust be proven to be well-defined. We use PROB’s WD analyser to computeWD(E). External Provers.As in RODIN, it is possible to interface to external provers, such as SMT solvers, namely Z3, the Atelier-B ML/P provers, the PROB constraint-based disprover, and the specialised PROB prover for WD conditions. The interfaces to the SMT solvers and the Atelier-B provers are already part of PROB and are reused. Calls to external provers can be time-consuming, so they are implemented as symbolic transitions to prevent all provers from being called each time a state is explored. 140Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover forPROB 5 Proving with PROB Figure 3: Rules as Transitions in the PROB Animator We integrated the proof rules into the PROB core, enabling di- rect loading of PO files exported with the PROB Disprover plugin from RODIN. The animator automatically enters the newsequent proveranimation mode, providing access to the proof transitions (Figure 3). With the animator, we obtain a user interface to the prover and full access to its debugging capabilities within the PROB tooling, e.g. via PROB2-UI [6]. We present new export options for proofs created with PROB. 8 The aim is twofold: to make the proof more comprehensible for the user and to enable it to be exported to other tools. 5.1 Save and Replay Proof Trace A proof created by PROB corresponds to a sequence of applied proof rules, i.e. alineartrace of transitions. Such a trace can be saved as a JSON file that contains all relevant steps, parameter values, and state terms for later replay with PROB. This also enables interactive trace replay [15], allowing a gradual and controlled replay of a proof. This can be advantageous in several scenarios, for instance, when proofs have to be refactored after small changes to the Event-B model, where only a few rules within a proof trace need to be replaced. It can be employed to replay a trace created for an abstract Event-B model on the refined model (or vice versa), therebyrefining the proofwithout having to perform it from scratch. Moreover, it is possible to save a trace of a partial proof and continue it later. 5.2 Visualisation PROB integrates various visualisation mechanisms. These include graph visualisations created with Graphviz [11] and state visualisations controlled either by an animation function or by VISB [31], which enables domain-specific visualisations based on SVG graphics. We use these interfaces to generate comprehensible proof representations and allow users to control the proof by clicking in the visualisation. Interactive State Visualisation.To represent the current proof state during animation, we use PROB’s state visualisation feature. The visualisation is grid-based, where each cell can contain text or an image. The cell contents are determined by a special Prolog predicate representing the animation function, with the current state as input. For our sequent prover, the animation function deconstructs the state into the current state and its continuations, displaying the current sequent in the leftmost column, with its continuations in the subsequent columns. In addition, the previous state is displayed next to the current state. See Fig- ure 4 for a visualisation of our example introduced in Section 2 in PROB2-UI. Selected hypotheses appear above the line, while the current goal is shown below. The predicates are rendered in a read- able manner using the pretty-printer for B expressions of PROB. Using its Unicode mode produces a representation that closely resembles mathematical notation. Additionally, a visualisation of the pre- vious sequent is provided for comparison of the changes made by the recent transition. The visual- isation is interactive, allowing the user to select a row in the current sequent by right-clicking on it. 8 Examples can be explored online at https://stups.hhu-hosting.de/models/sequent prover. K. Engels, J. Gruteser, and M. Leuschel141 Figure 4: Visualisation of the Current and Previous Proof Sequent with Applicable Rules for One Row The applicable rules for the selected row can be accessed via a pop-up menu, using the associated transi- tion descriptions (cf.Section 4). In comparison, RODINallows direct application of manual rewrite rules by clicking on symbols highlighted in red within a formula. Here, the currently applicable rules can be se- lected via the operations view, and the already performed steps can be inspected in the history. The state visualisation is accompanied by the state view, which lists the current hypotheses and the goal. Proof Tree.With the PROB animator, proofs (or proof attempts) are represented as traces leading to the current state (cf. Section 5.1), with open proof nodes represented by continuations in that state. However, the user can also skip to a continuation during the animation, so that a trace does not itself provide a proof tree. Hence, we implemented a conversion from a prooftraceto atreerepresentation. This can then be visualised using the interface from PROB to Graphviz, and is used for exporting proofs (see Section 5.3). Converting a linear proof trace into a proof tree involves creating nodes for each continuation, with edges representing the applied proof rules. Each edge links a sequent to its new continuations resulting from the application of the rule. When a rule discharges the goal, the corresponding edge connects to a node representing the successful proof for that branch. We integrated a visualisation of the proof tree in PROB’s graph visualisations, easily accessible via the user interfaces (e.g. CLI, PROB2-UI). It allows users to inspect the current state in the context of the proof tree. An example is shown in Figure 5. By interfacing with Graphviz, the visualisation can be exported in multiple other file formats, including PDF, SVG, PNG, or as raw DOT file. Interactive HTML Documents.Often, proofs are hard-wired to a specific tool and cannot be exported easily. For instance, RODINstores proofs as raw XML data in .bpr files, limiting the ability to share the proof outside of the tool. In contrast, PROB allows to export traces of formal models with state visualisations as standalone HTML documents. However, the existing export options are not ideally suited for proofs. To address this, we developed a new HTML export based on the proof tree. Note that the HTML file generation is also implemented in Prolog. Hereby, we generate an SVG visualisation of the proof tree using Graphviz. Our visualisation highlights which parts of the sequent have changed after a proof step. Users can manually adjust their view by zooming and panning. In addition, we list the applied proof rules, i.e. the edges of the proof tree, next to the visualisation. Users can interactively click on proof steps to enlarge the relevant parts of the tree and navigate through it step by step. Figure 5 shows a screenshot of an example. Rule 8 has been selected, corresponding to the right branch in the enlarged section of the visualisation. The green triangle indicates that the applied proof rule (fun goal) has discharged the goal, and this branch of the proof tree is complete. The left branch has not yet been proven, and can be explored either by panning in the visualisation or by navigating to the next step in the step view. In general, the export allows a detailed and interactive inspection of the applied proof steps and the proof tree itself. It is particularly useful for teaching because adjacent proof nodes are displayed clearly in the proof tree, unlike in the visualisation in RODIN. Also, only a web browser is required to inspect a proof. 142Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover forPROB Figure 5: Interactive HTML Proof Tree Figure 6: Proof replayed by the Sequent Prover in RODIN 5.3 Export for Replay with Rodin In addition to the human-readable HTML outputs, we developed an XML export for proof replay within RODIN. RODINstores proof trees, along with the applied steps and the associated Java reasoners, in BPR files, which are based on XML. For our examples, complete BPR files can be found on the web server. To export a proof, we generate a BPR file in Prolog based on our proof tree (cf. Section 5.2), transforming proof nodes into continuations and edges into proof rule applications. In addition, the required Java reasoners are specified, which are called by RODINduring the replay of the proof. If the RODINreasoners can replay a proof created with PROB, we obtain additionalvalidation of the proof, enabling PROB to be used as asecond chain. Users can also export a partial proof from PROB to RODIN, yielding a more detailed proof tree in RODIN(see Figure 6), instead of nodes that apply several steps at once. For example, when the ML (Mono Lemma) prover from ATELIER-B discharges a goal in RODIN, the applied tactics remain completely hidden from the user (compared to Figure 6, there would be just a single success node with no further details). Furthermore, unlike a pure RODINproof, our export includes the precise rule names as comments. However, there are still a few limitations in the mapping of our proof rules to the RODINreasoners. Specifically, many of the automatic rewrite rules cannot be translated from our detailed proof steps, since RODINapplies most of the simplification rules recursively in one step to all hypotheses and conceals them behind the message “simplification rewrites”. For these rules, we generate individual proof steps that are marked as “reviewed” (the step is actually reviewed by PROB), enabling unverified replay in RODIN. The same approach is used for our custom rules without an equivalent in RODIN. This can be observed in Figure 6, where we used the PROB sequent prover to apply the ruleFIN FUNDOM, which is not yet implemented in RODIN. While the replay succeeds using the aforementioned review, it is not possible to perform the same proof with RODINstandalone. K. Engels, J. Gruteser, and M. Leuschel143 5.4 Automated Proving Model CheckingOne can use PROB’s model checker as an automatic prover. This can be useful to find proofs, but performance-wise this is not ideal: the model checker will store every reached proof state and will always compute all possible applications of proof rules for an explored proof state. Auto ProverLuckily, search is one of the strengths of Prolog. As such, it is easy to encode a custom proof search on top of our Prolog encoding of the Event-B proof rules. We have thus implemented a first automatic prover, using iterative deepening search with a few simple heuristics. The heuristics describe “eager” proof rules that should always be applied (deterministically first) likeANDRandANDL to decompose conjunctions in the proof goal and in the hypotheses. This prover is already useful to automatically find short proofs (it can be run automatically in our animator interface). In the future, we wish to encode more clever heuristics and enforce ordering of the proof rules. By using partial evaluation, we expect to obtain a very fast, rule-based prover for Event-B which ideally will surpass the performance of current provers like the ML prover from ATELIER-B. Indeed, ATELIER-B uses thetheory languageto express proof rules, which can be viewed as domain specific logic “programming language” tailored to B and proof. While ATELIER-B comes with a custom developed compiler – theLogic Solver– it seems like it cannot compete with state-of-the-art Prolog compilers (see [22], in particular Section 6). This suggests that, at least in principle, our Prolog encoding could lead to a faster automated prover. 6 Comparison with Java Implementation Using Prolog for verification tools has been advocated by Leuschel [21, 23]. In this section we compare our Prolog implementation with the existing Java implementation of the Event-B proof rules. The RODINplatform has now been developed for well over 20 years. Our sequent prover was devel- oped since summer 2025 during a 20 ETCS credit points project by the first author (i.e., about 600 hours of work), with additional developments by the other authors (notably on proof visualisation, export and auto-proving). Table 1 provides a brief overview of the Java source code of the sequent prover compared to our Prolog implementation. 9 Note that the intention of this table is to give a rough estimate of the size of the implementation. Table 1: Statistics of Java and Prolog Implementation ToolLanguageCode for Sequent ProverMissing Rules FilesLOCSLOCRewriteInference RODINJava320501822758055/53616/123 PROBProlog4420837054/5368/123 Our implementation covers more proof rules (not counting the additional proof rules taken from [2] as well as few additional ones for Peano arithmetic). In terms of code size there is an order of magnitude difference when counting lines of code (LOC) and a bit less when counting source lines of code (SLOC, i.e., disregarding comments and whitespace). 9 The columns SLOC (Source Lines of Code) was generated using David A. Wheeler’s ‘SLOCCount’ tool. The tool also computes an estimated number of person years: 6.51 for the Rodin sequent prover and 0.79 for our prover. At least the latter number is quite close to the real development effort. 144Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover forPROB In general, new proof rules can be added easily to our Prolog implementation, sometimes requiring a single clause as opposed to a new class in Java. Consider for example theDERIVDOMTOTALRELrule we have used in Section 2. The Prolog clause just expresses the logical condition when the domain of a total relation can be rewritten (cf. top of Listing 4). Beyond this logical core, the Java implementation involves the construction of many objects and various additional checks. It also distinguishes explicitly between rewriting in goals and hypotheses, which we do not have to do in Prolog. This leads to a class of 257 LOC compared to one clause in Prolog (which facilitates maintenance). It is also indicative (and maybe not surprising) that the Java implementation is still missing 71 proof rules, 20 years on. While the exact reason for this is unclear to us, it at least suggests that non-trivial development effort is required to add new proof rules in Java. Earlier work by Leuschel [22] has shown several orders of magnitude difference between another Prolog prover and running the RODINprovers. The prover presented there, however, is a dedicated prover for well-definedness and is not complete (it typically does not do case distinctions to avoid ex- ponential blow-up). Our prover presented in this paper is not yet tuned for performance, and the tactics of the auto-prover need to be fully implemented. Therefore, we have not yet tested whether the Prolog implementation of the proof rules or the Java counterpart is more efficient. In the future, we intend to re-use the hypothesis management from [22], along with partial evaluation to obtain an efficient, yet ex- tensible and maintainable prover. We also plan to incorporate custom proof rules written by users using RODIN’s theory plugin [8]. 7 Teaching Aspects Modelling the mars rover was a project in our university course on safety-critical systems, where students learn the development and verification of reliable software using the formal B method. The system is considered safety-critical due to financial concerns, as damage to or loss of the rover would result in significant costs. Using the interactive sequent prover can provide insight into the reasoning behind proofs that are otherwise discharged automatically in RODIN. The existence of different ways to provide a successful proof is another reason why interactive exploration is useful for teaching. With the PROB sequent prover, we could prove all proof obligations of a machine from the self- developed model. On the contrary, proving preservation of the same invariants was rather challenging in RODIN, although we knew why the invariants must hold after execution of the events. Some proofs went through after clicks through symbols and the repeated pruning of proof branches, which did not help to gain a clear understanding of why the proof succeeded. This experience allows us to assume, that using our prover improves the user experience from an educational point of view, as the effect of each applied rule is visible. Together with our HTML proof export, students can focus on proof rules instead of specific tool buttons and can examine the interaction of the rules more systematically. For future work, we are considering “gamification” of the animation to give more insights, for ex- ample by using heuristics to provide additional guidance on promising rules in the current state, and restricting the set of available rules. There are similar approaches, for instance, Hendriks et al. [17] developed an interactive web interface for teaching logic based on the proof assistant Coq. Cumbor et al. [9] conducted a “proof game” approach for inference rules, which they report as being popular among students. Another example of proof gamification is Kevin Buzzard’s Natural Number Game for Lean 10 , which introduces the writing of formal proofs in Lean by interactive exercises. A recent study analysed the interaction of undergraduate students with the tool [18]. 10 https://adam.math.hhu.de/#/g/leanprover-community/nng4 K. Engels, J. Gruteser, and M. Leuschel145 8 Related Work The work by Grieu et al. [14] translates RODINproofs to the TLA + Proof System (TLAPS). They encountered the issue that RODINapplies many simplification rules together in a single step, making a translation challenging (as described in Section 5.3). Our more fine-grained proof trees would solve this problem (and Prolog would be a good language to encode such translation rules). The Why3 Plug-In for RODIN[19] translates proof obligations into Why3, but proofs are not trans- lated back to Event-B proofs. Here the Dedukti research project [4] is more relevant: it has the goal to share proofs across systems. Some first works try to translate B/Event-B proofs to theλΠ-Calculus [30, 13]. Our work helps understand, visualise and check proofs, but is based on a translation to a program- ming language (Prolog) rather than a proof calculus. As already discussed in Section 5.4, Atelier-B uses a domain-specific “theory language” to express the proof rules. The execution engine (krt) written in C seems to have a performance far below that of mature Prolog engines (see [22]). There are many successful interactive provers, a.k.a. proof assistants such as Coq, PVS, Lean and Isabelle/HOL. A translation of Event-B to Isabelle was studied by Schmalz [29]. The work was never completed to a point where one could use Isabelle for arbitrary proof obligations. LeanTAP [5, 10] is a theorem prover for first-order logic written in a few lines of Prolog. Its per- formance is one inspiration for our work. Another successful prover is Vampire [28]. LeanTAP and Vampire are based mainly on resolution, while in this work we have encoded many different B-specific proof rules. One interesting question is whether Prolog or a term rewriting system such as Maude is more ap- propriate to encode our proof rules. Prolog supports full unification, but only at the top-level of a term, while term rewriting systems support matching and rewriting of subterms. For most of our inference rules, unification at the top-level was sufficient, e.g., forAND Rin Section 2 which looks for an outer conjunction in a proof goal. The simplification rules, however, require traversing the proof goal or the hypotheses for matching subterms. This traversal is encoded in one separate predicate; the simplifica- tion rule encodings again match at the top-level. We are not aware of any efforts to encode B proof rules in term-rewriting systems. The BMaude tool [7] provided support for executing a subset of classi- cal B in Maude, but according to past experiments it was considerably slower than PROB. 11 The newer EventB2Maude tool [27] supports Event-B and provides some inference rules for probabilistic reasoning. 9 Conclusion In summary, we have implemented a new sequent prover for the Event-B formal method. The implemen- tation covers more than 600 proof rules, and after 9 months of development it covers more of the standard proof rules than the previous Java implementation after 20 years. The code is an order of magnitude more compact and should be easier to maintain and extend in the future. By integrating the proof rules into PROB, we have managed to use the animation features of PROB for interactive proving, proof replay and proof repair. New visualisation and HTML export features have been added to PROB, enabling bet- ter human understanding of proofs. A preliminary automated prover is implemented and proofs can be re-exported and double-checked in the RODINplatform. 11 E.g., 8.6 seconds vs 0.9 seconds to model check a mutual exclusion B model with 8008 states. Experiment conducted by the last author in August 2018. 146Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover forPROB References [1] Jean-Raymond Abrial (2005):The B-Book: Assigning Programs to Meanings. Cambridge University Press. [2] Jean-Raymond Abrial (2010):Modeling in Event-B: System and Software Engineering. Cambridge Univer- sity Press. [3] Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta & Laurent Voisin (2010):Rodin: An Open Toolset for Modelling and Reasoning in Event-B.Int. J. Softw. Tools Technol. Transf.12(6), p. 447–466, doi:10.1007/s10009-010-0145-y. [4] Ali Assaf, Guillaume Burel, Rapha ̈ el Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Fr ́ ed ́ eric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard (2023):Dedukti: a Logical Framework based on theλΠ-Calculus Modulo Theory.CoRRabs/2311.07185, doi:10.48550/ARXIV.2311.07185. arXiv:2311.07185. [5] Bernhard Beckert & Joachim Posegga (1995):leanTAP: Lean Tableau-based Deduction.J. Autom. Reason- ing15(3), p. 339–358, doi:10.1007/BF00881804. [6] Jens Bendisposto, David Geleßus, Yumiko Jansing, Michael Leuschel, Antonia P ̈ utz, Fabian Vu & Michelle Werth (2021):ProB2-UI: A Java-based User Interface for ProB. In:Proceedings FMICS, LNCS 12863, p. 193–201, doi:10.1007/978-3-030-85248-1 12. [7] Christiano Braga & Narciso Mart ́ ı-Oliet (2021):B Maude: A formal executable environment for Abstract Machine Notation Descriptions.CoRRabs/2108.07878. arXiv:2108.07878. [8] Michael J. Butler & Issam Maamria (2013):Practical Theory Extension in Event-B. In:Theories of Pro- gramming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, p. 67–81, doi:10.1007/978-3-642-39698-4 5. [9] David Cumbor, Bill Stoddart & Steve Dunne (2010):Teaching Logic Proofs for Formal Aspects. In Chris- tian Attiogb ́ e & Dominique M ́ ery, editors:Colloque ”From Research to Teaching Formal Methods: The B Method” (TFM-B’2010), APCB, Nantes, France, p. 2–16. Available at https://hal.science/hal-04993432v1. [10] Melvin Fitting (1998):leanTAP Revisited.J. Log. Comput.8(1), p. 33–47, doi:10.1093/logcom/8.1.33. [11] Emden R. Gansner (2011):Drawing graphs with Graphviz. Technical Report. [12] Gerhard Gentzen (1935):Untersuchungen ̈ uber das logische Schließen. I.Mathematische Zeitschrift39(1), p. 176–210, doi:10.1007/BF01201353. [13] Anne Grieu (2024):From Event-B to Lambdapi. In:Proceedings ABZ, p. 387–391, doi:10.1007/978-3- 031-63790-2 29. [14] Anne Grieu, Jean-Paul Bodeveix & Mamoun Filali (2025):Translating Event-B Models and Development Proofs to TLA+. In:Proceedings ABZ, LNCS 15728, Springer, p. 124–142, doi:10.1007/978-3-031-94533- 5 8. [15] Jan Gruteser & Michael Leuschel (2025):Interactive Trace Replay for Event-B Models. In:12th Rodin User and Developer Workshop. Available at https://eprints.soton.ac.uk/id/eprint/503334. [16] Jan Gruteser, Michael Leuschel, Katharina Engels & Fabian Vu (2026):Animation, Verification and Visuali- sation of Prolog Transition Systems with ProB. In:Proceedings ICLP, EPTCS. To appear. [17] Maxim Hendriks, Cezary Kaliszyk, Femke van Raamsdonk & Freek Wiedijk (2010):Teaching logic using a state-of-the-art proof assistant.Acta Didactica Napocensia3. [18] Paola Iannone & Athina Thoma (2025):‘It Feels Like Sort of Cheating in Some Ways that You Don’t Fully Show that You’ve Understood the Proofs’: Mathematics Students Coding Proofs with An Interactive Theorem Prover.Digital Experiences in Mathematics Education, p. 1–27, doi:10.1007/s40751-025-00193-w. [19] Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah & Alexander B. Romanovsky (2016):Rodin Plat- form Why3 Plug-In. In:Proceedings ABZ 2016, LNCS 9675, p. 275–281, doi:10.1007/978-3-319-33600- 8 21. K. Engels, J. Gruteser, and M. Leuschel147 [20] Sebastian Krings, Jens Bendisposto & Michael Leuschel (2015):From Failure to Proof: The ProB Disprover for B and Event-B. In:Proceedings SEFM 2015, LNCS 9276, Springer, p. 199–214, doi:10.1007/978-3- 319-22969-0 15. [21] Michael Leuschel (2008):Declarative Programming for Verification: Lessons and Outlook. In:Proceedings PPDP’2008, ACM Press, p. 1–7, doi:10.1145/1389449.1389450. [22] Michael Leuschel (2020):Fast and Effective Well-Definedness Checking. In:Proceedings iFM 2020,LNCS 12546, Springer, p. 63–81, doi:10.1007/978-3-030-63461-24. [23] Michael Leuschel (2020):Prolog for Verification, Analysis and Transformation Tools. In:Proceedings VPT 2020, EPTCS 320, p. 80–94, doi:10.4204/EPTCS.320.6. [24] Michael Leuschel (2023):ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. In:Prolog: The Next 50 Years, LNCS 13900, Springer, p. 239–247, doi:10.1007/978-3-031-35254- 619. [25] Michael Leuschel & Michael J. Butler (2008):ProB: an automated analysis toolset for the B method.STTT 10(2), p. 185–203. Available at http://dx.doi.org/10.1007/s10009-007-0063-9. [26] Patrick Lincoln & Jim Christian (1989):Adventures in Associative-Commutative Unification.Journal of Symbolic Computation8(1-2), p. 217–240, doi:10.1016/S0747-7171(89)80026-4. [27] Carlos Olarte, Daniel Osorio, Carlos Ram ́ ırez & Camilo Rocha (2025):Algorithmic Analysis of Event-B in Rewriting Logic. In:Proceedings NFM 2025, LNCS 15682, p. 275–293, doi:10.1007/978-3-031-93706- 416. [28] Alexandre Riazanov & Andrei Voronkov (2002):The design and implementation of VAMPIRE.AI Commun. 15(2-3), p. 91–110. Available at http://content.iospress.com/articles/ai-communications/aic259. [29] Matthias Schmalz (2012):Formalizing the logic of event-B: Partial functions, definitional extensions, and au- tomated theorem proving. Ph.D. thesis, ETH Zurich, Z ̈ urich, Switzerland, doi:10.3929/ETHZ-A-007577749. Available at https://hdl.handle.net/20.500.11850/64337. [30] Claude Stolze, Olivier Hermant & Romain Guillaum ́ e (2024):Towards Formalization and Sharing of Atelier B Proofs with Dedukti. Available at https://hal.science/hal-04398119. Working paper or preprint. [31] Michelle Werth & Michael Leuschel (2020):VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. In:Proceedings ABZ,LNCS12071, Springer, p. 260–265, doi:10.1007/978-3-030-48077-621. The source code is available insrc/sequentproveras part of ProB’s source code: https://stups. hhu-hosting.de/downloads/prob/source.

Instant research discovery