Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B Katharina Engels
Jan Gruteser
Michael Leuschel
Faculty of Mathematics and Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universitätsstr. 1, D-40225 Düsseldorf {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 P RO B, 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 P RO B, an interactive HTML document for tool-independent exploration of the proof tree, and an export back to RODIN, allowing the P RO B 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 EventB 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 RODIN platform [3], which also caters for several industrial and academic plugins to automatically conduct proofs. The RODIN platform 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. Export POs The initial motivation of this work for ProB POs as Proof Rules came from teaching. While the EventRodin Prolog Facts in Prolog B proof rules are discussed in detail .pl Load via during lectures and are presented in the XTL Interface literature [2], RODIN often applies sev- Replay Replay eral proof steps simultaneously. The Trace plugins of RODIN also conduct an en.bpr Proof ProB Animator tire proof in a single step. In both manual/ State Visualisation .html autom. cases, the user or student cannot easily check, understand or reproduce a proof. Figure 1: Architecture of P RO B’s Sequent Prover Hence, the initial intention was to develop 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 W. Faber, L. Giordano, R. Rocha, V. Santos Costa (Eds.): 42nd International Conference on Logic Programming (ICLP 2026) EPTCS 450, 2026, pp. 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.
K. Engels, J. Gruteser, and M. Leuschel
135
for advanced users: a second independent toolchain to double-check proofs, new visualisation and analysis 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 rules1 , but also a few additional rules proposed by Abrial [2]. Within the RODIN platform, 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 P RO B 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 RODIN proof files (BPR) in XML format, we close the loop to the RODIN prover, enabling the P RO B 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 RODIN tool 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 P RO B, featuring – an interactive sequent prover using the P RO B animator, along with an interactive visualisation showing the current proof sequent, – an export of a proof tree visualisation as interactive HTML document using P RO B’s interface to Graphviz for detailed analysis and teaching, – an export of a proof as BPR file for replay in the RODIN platform, • 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 obligations arise, for example, from invariants, refinement, user-specified theorems or well-definedness conditions such as potential divisions by zero.2 Depending on the type of a PO, a selection of hypotheses H is available to prove the goal G. Formally, a PO can be represented by a sequent H ⊢ G. This sequent expresses that the goal G logically follows from the set of hypotheses H using the proof rules of Event-B. 1 https://wiki.event-b.org/index.php/Inference Rules/All Rewrite Rules 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.
136
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B
One can use a set of different inference rules to prove a sequent. One of these rules is the HYP 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: AND R
H ⊢ P H ⊢ Q H ⊢ P∧Q
H, f ∈ E → F ⊢ f ∈ TypeE → 7 TypeF
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 that f is a partial function (→ 7 symbol) if it is a total function (→ symbol) for some domain E and range F. We use an example PO from an Event-B mars rover model3 that will be used throughout the next chapters. A safety invariant states that the rover must not be exposed to excessive radiation, expressed by radiation(rover) ≤ αmax , where radiation assigns a radiation value to a position. For this invariant, a well-definedness (WD) PO is created, as function application is only defined if radiation is actually a function and rover is in the domain of radiation. A complete proof of the WD PO is depicted 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 the AND R rule. To discharge the first resulting sequent at the top, we apply the FUN GOAL rule following from the first hypothesis. For the next sequent, we apply a rule for total relations and functions (DERIV DOM TOTALREL) to remove the domain operator dom from the goal. The second hypothesis contains a singleton set and can be simplified using the SIMP SUBSETEQ SING rule, after which we can discharge the goal by using the HYP rule.
radiation ∈ field → N {rover} ⊆ field ⊢ radiation ∈ Z × Z → 7 Z ∧ rover ∈ dom(radiation)
radiation ∈ field → N {rover} ⊆ field ⊢ radiation ∈ Z × Z → 7 Z
FUN GOAL
Proven
Proven HYP
AND R
radiation ∈ field → N {rover} ⊆ field ⊢ rover ∈ dom(radiation)
DERIV DOM TOTALREL
radiation ∈ field → N {rover} ⊆ field ⊢ rover ∈ field
SIMP SUBSETEQ SING
radiation ∈ field → N rover ∈ field ⊢ rover ∈ field
Figure 2: Application of Inference and Rewrite Rules to Prove a PO
3
State-Based Representation of Proof Obligations
P RO B [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 P RO B [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 predicate trans(Label,StateBefore,StateAfter), where the states of a transition system are represented as Prolog terms. The initial states are provided using the start(State) predicate. State properties can be specified with prop(State,Property). Here, we use them for better comprehensibility only. In the following, we use P RO B’s XTL mode to turn the Event-B proof rules into an animatable transition system. 3 Available at https://stups.hhu-hosting.de/models/sequent prover. 4 Detailed documentation at: https://prob.hhu.de/w/index.php?title=Other languages.
K. Engels, J. Gruteser, and M. Leuschel The code in Listing 1 demonstrates the XTL functionality for a simple button. Initially, the button is on and can be toggled to the other state via a transition. The property shows the current state of the button.
137
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).
For our sequent prover, the state representation is slightly more complex. An example is shown in Listing 2, illustrating the Prolog representation 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 entry SelHyps; the current Goal is 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. The continuation Cont is either success or is the next still unproven sequent (which has another continuation itself). In the initial state, there is exactly one open goal, so the continuation is success. If the current state becomes success, then the proof has succeeded and there are no more open goals to show. The Info field 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 P RO B is not yet capable of generating proof obligations (POs)6 , we use the RODIN platform for generation of POs for Event-B specifications. Using the P RO B 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 form disprover_po(Label,Context,Goal,AllHyps,SelHyps,Status). This format was originally designed for the P RO B Disprover [20]. Hence, we can easily reuse it to load and convert the POs for our sequent prover within P RO B. 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). The Goal is represented as an untyped abstract syntax tree (AST) as are all available hypotheses in AllHyps and pre-selected ones in SelHyps. Status contains the RODIN proof status. The Context is 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 P RO B’s WD prover [22]. Using the same format as the WD prover facilitates the integration of the proof rules into the P RO B core. Then, the normalised hypotheses are combined with the goal into a term that represents the initial state of the PO as shown in Listing 2. Finally, all POs of a machine are made available as initial states together with their corresponding label start(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.
138
4
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B
Proof Rules as a Transition System
To define how proof rules transform a sequent into another or more successor sequents, the transition predicate that was introduced in the previous section can be used. Take for example the rule SIMP SUBSETEQ SING we applied in Section 2. It encodes {E} ⊆ 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 for simp rule, 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 like DERIV DOM TOTALREL, where the rule needs access to all hypotheses. Note that in member(member(R,RType),Hyps), the inner member represents 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. Leuschel
139
• We show the encoding of the AND R rule, which decomposes the goal conjunct(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 by add goals in line 8 of Listing 4). • We have axioms as terminal proof steps, which close a proof branch without generating successor sequents, e.g. HYP and FUN GOAL. HYP is applied whenever the current goal is already contained in the hypotheses, i.e., when unification succeeds. One must consider that Prolog unification is insufficient for associative-commutative operations to determine equality [26]. Expressions such as add(add(x,y),z) and add(x,add(y,z)) or add(add(z,y),x) cannot be unified directly. Instead, in member hyps ground terms are then normalised 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, HYP can be applied for y < x ⊢ x ≥ y. The applicability of fun goal depends on the goal having a particular form. type expression 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 metainformation. 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 in Info. 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)) in member('$'(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 ∈ S with a fresh identifier x. 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. P RO B allows to add dynamic transition properties depending on the parameter 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 property description/1. These are used to display the transition descriptions in P RO B2-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 hypotheses 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 use symbolic transitions specified by the predicate symb trans/3 in a similar way as for trans/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 expression E for the instantiation. In addition, E must be proven to be well-defined. We use P RO B’s WD analyser to compute WD(E). External Provers. As in RODIN, it is possible to interface to external provers, such as SMT solvers, namely Z3, the Atelier-B ML/PP provers, the P RO B constraint-based disprover, and the specialised P RO B prover for WD conditions. The interfaces to the SMT solvers and the Atelier-B provers are already part of P RO B 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.
140
5
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B
Proving with P RO B
We integrated the proof rules into the P RO B core, enabling direct loading of PO files exported with the P RO B Disprover plugin from RODIN. The animator automatically enters the new sequent prover animation 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 P RO B tooling, e.g. via P RO B2-UI [6]. We present new export options for proofs created with P RO B.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
5.2
Visualisation
Figure 3: Rules as Transitions in the P RO B Animator A proof created by P RO B corresponds to a sequence of applied proof rules, i.e. a linear trace 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 P RO B. 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), thereby refining the proof without having to perform it from scratch. Moreover, it is possible to save a trace of a partial proof and continue it later.
P RO B integrates various visualisation mechanisms. These include graph visualisations created with Graphviz [11] and state visualisations controlled either by an animation function or by V IS B [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 P RO B’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 Figure 4 for a visualisation of our example introduced in Section 2 in P RO B2-UI. Selected hypotheses appear above the line, while the current goal is shown below. The predicates are rendered in a readable manner using the pretty-printer for B expressions of P RO B. Using its Unicode mode produces a representation that closely resembles mathematical notation. Additionally, a visualisation of the previous sequent is provided for comparison of the changes made by the recent transition. The visualisation 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. Leuschel
141
The applicable rules for the selected row can be accessed via a pop-up menu, using the associated transition descriptions (cf. Section 4). In comparison, RODIN allows direct application of manual rewrite rules by clicking on symbols highlighted Figure 4: Visualisation of the Current and Previous Proof in red within a formula. Here, the Sequent with Applicable Rules for One Row currently applicable rules can be selected 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 P RO B 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 proof trace to a tree representation. This can then be visualised using the interface from P RO B 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 P RO B’s graph visualisations, easily accessible via the user interfaces (e.g. CLI, P RO B2-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, RODIN stores proofs as raw XML data in .bpr files, limiting the ability to share the proof outside of the tool. In contrast, P RO B 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.
142
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B
Figure 5: Interactive HTML Proof Tree
5.3
Figure 6: Proof replayed by the Sequent Prover in RODIN
Export for Replay with Rodin
In addition to the human-readable HTML outputs, we developed an XML export for proof replay within RODIN. RODIN stores 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 RODIN during the replay of the proof. If the RODIN reasoners can replay a proof created with P RO B, we obtain additional validation of the proof, enabling P RO B to be used as a second chain. Users can also export a partial proof from P RO B 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 RODIN proof, 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 RODIN reasoners. Specifically, many of the automatic rewrite rules cannot be translated from our detailed proof steps, since RODIN applies 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 P RO B), 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 P RO B sequent prover to apply the rule FIN FUN DOM, 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 RODIN standalone.
K. Engels, J. Gruteser, and M. Leuschel
5.4
143
Automated Proving
Model Checking One can use P RO B’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 Prover Luckily, 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) like AND R and AND L 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 the theory language to 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 – the Logic 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 RODIN platform has now been developed for well over 20 years. Our sequent prover was developed 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 Tool
Language
RODIN P RO B
Java Prolog
Code for Sequent Prover Files LOC SLOC 320 50182 27580 4 4208 3705
Missing Rules Rewrite Inference 55/536 16/123 4/536 8/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.
144
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B
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 the DERIV DOM TOTALREL rule 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 RODIN provers. 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 exponential 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 extensible 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 P RO B sequent prover, we could prove all proof obligations of a machine from the selfdeveloped 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 example 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 Lean10 , 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. Leuschel
8
145
Related Work
The work by Grieu et al. [14] translates RODIN proofs to the TLA+ Proof System (TLAPS). They encountered the issue that RODIN applies 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 translated 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 programming 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 performance 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 appropriate 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., for AND R in 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 simplification 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 classical B in Maude, but according to past experiments it was considerably slower than P RO B.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 implementation 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 P RO B, we have managed to use the animation features of P RO B for interactive proving, proof replay and proof repair. New visualisation and HTML export features have been added to P RO B, enabling better human understanding of proofs. A preliminary automated prover is implemented and proofs can be re-exported and double-checked in the RODIN platform. 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.
146
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for P RO B
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 University 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ël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard (2023): Dedukti: a Logical Framework based on the λ Π-Calculus Modulo Theory. CoRR abs/2311.07185, doi:10.48550/ARXIV.2311.07185. arXiv:2311.07185. [5] Bernhard Beckert & Joachim Posegga (1995): leanTAP: Lean Tableau-based Deduction. J. Autom. Reasoning 15(3), pp. 339–358, doi:10.1007/BF00881804. [6] Jens Bendisposto, David Geleßus, Yumiko Jansing, Michael Leuschel, Antonia Pütz, Fabian Vu & Michelle Werth (2021): ProB2-UI: A Java-based User Interface for ProB. In: Proceedings FMICS, LNCS 12863, pp. 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. CoRR abs/2108.07878. arXiv:2108.07878. [8] Michael J. Butler & Issam Maamria (2013): Practical Theory Extension in Event-B. In: Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pp. 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 Christian Attiogbé & Dominique Méry, editors: Colloque ”From Research to Teaching Formal Methods: The B Method” (TFM-B’2010), APCB, Nantes, France, pp. 2–16. Available at https://hal.science/hal-04993432v1. [10] Melvin Fitting (1998): leanTAP Revisited. J. Log. Comput. 8(1), pp. 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 über das logische Schließen. I. Mathematische Zeitschrift 39(1), pp. 176–210, doi:10.1007/BF01201353. [13] Anne Grieu (2024): From Event-B to Lambdapi. In: Proceedings ABZ, pp. 387–391, doi:10.1007/978-3031-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, pp. 124–142, doi:10.1007/978-3-031-945335 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 Visualisation 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 Napocensia 3. [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, pp. 1–27, doi:10.1007/s40751-025-00193-w. [19] Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah & Alexander B. Romanovsky (2016): Rodin Platform Why3 Plug-In. In: Proceedings ABZ 2016, LNCS 9675, pp. 275–281, doi:10.1007/978-3-319-336008 21.
K. Engels, J. Gruteser, and M. Leuschel
147
[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, pp. 199–214, doi:10.1007/978-3319-22969-0 15. [21] Michael Leuschel (2008): Declarative Programming for Verification: Lessons and Outlook. In: Proceedings PPDP’2008, ACM Press, pp. 1–7, doi:10.1145/1389449.1389450. [22] Michael Leuschel (2020): Fast and Effective Well-Definedness Checking. In: Proceedings iFM 2020, LNCS 12546, Springer, pp. 63–81, doi:10.1007/978-3-030-63461-2 4. [23] Michael Leuschel (2020): Prolog for Verification, Analysis and Transformation Tools. In: Proceedings VPT 2020, EPTCS 320, pp. 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, pp. 239–247, doi:10.1007/978-3-031-352546 19. [25] Michael Leuschel & Michael J. Butler (2008): ProB: an automated analysis toolset for the B method. STTT 10(2), pp. 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 Computation 8(1-2), pp. 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, pp. 275–293, doi:10.1007/978-3-031-937064 16. [28] Alexandre Riazanov & Andrei Voronkov (2002): The design and implementation of VAMPIRE. AI Commun. 15(2-3), pp. 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 automated theorem proving. Ph.D. thesis, ETH Zurich, Zürich, Switzerland, doi:10.3929/ETHZ-A-007577749. Available at https://hdl.handle.net/20.500.11850/64337. [30] Claude Stolze, Olivier Hermant & Romain Guillaumé (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, LNCS 12071, Springer, pp. 260–265, doi:10.1007/978-3-030-48077-6 21.
The source code is available in src/sequent prover as part of ProB’s source code: https://stups. hhu-hosting.de/downloads/prob/source.