Pith. sign in

REVIEW 2 major objections 5 minor 30 references

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

T0 review · 2 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A Prolog re-encoding turns Event-B's 600+ proof rules into explicit, inspectable proof steps inside ProB, making formal proofs teachable and reusable.

desk verdict A solid, useful tool paper: the Prolog encoding of Event-B rules into ProB is a real engineering accomplishment and the teaching/visualisation angle is genuinely nice, but the soundness of the rule encodings is more asserted than verified, and the 'second chain' phrasing in the abstract oversells what the Rodin export actually does. read the letter →

arxiv 2607.21191 v1 pith:SSD7UJHR submitted 2026-07-23 cs.LO cs.AIcs.SE

Katharina Engels (Heinrich Heine University Düsseldorf) , Jan Gruteser (Heinrich Heine University Düsseldorf) , Michael Leuschel (Heinrich Heine University Düsseldorf) This is my paper
classification cs.LOcs.AIcs.SE MSC 03B3568Q60
keywords Event-BsequentcalculusPrologProBinteractivetheoremprovingproofrulestreevisualisationRodin
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that the Event-B proof calculus can be faithfully re-implemented as a Prolog transition system, and that doing so yields a practical interactive prover. It encodes more than 600 inference and rewrite rules in about 4,200 lines of Prolog, an order of magnitude less code than Rodin's Java implementation, while covering more rules. This makes every proof step a visible transition: the user, or a student, can apply rules one at a time, inspect the current sequent, and see how the proof tree grows. The same proof can be exported as an interactive HTML document, replayed in Rodin via BPR files, or repaired after small model changes, which supports both teaching and a second-chain validation of Rodin proofs. If the encoding is faithful, the tool gives Event-B a transparent, extensible, and potentially very fast proof engine.

What carries the argument

The central mechanism is the labelled transition system: sequents are Prolog terms (state/sequent with selected hypotheses, goal, and a continuation for open branches), and proof rules are clauses of the trans/3 predicate. Rewrite rules are factored through simp_rule, and terminal rules such as HYP are handled as axioms. For associative-commutative equality in the HYP rule, ground terms are normalised into flat lists and compared by sorting rather than by direct unification, and hypotheses are allowed to be stronger than the goal. This lets the full proof rule set act as executable, animatable code.

What would settle it

Construct an invalid sequent whose goal is an associative-commutative equality (or a 'stronger hypothesis' case) that the sorting-based comparison in the HYP rule would wrongly accept, and run the prover on it: if the tool closes the branch with HYP, the encoding is unsound. For example, take a sequent where the hypothesis is y < x and the goal is x ≥ y (which is valid), then try a deliberately invalid variant such as x < y with goal x ≥ y and check whether HYP is rejected.

Watch

Extended reading notes

Core claim

We have implemented a new sequent prover for the Event-B formal method in Prolog, covering more than 600 proof rules. By integrating these rules into the Prolog-based animator ProB, each rule application becomes a labelled transition between sequent states, so proof construction is explicitly visible and user-controllable. The implementation is about an order of magnitude more compact than the Java implementation in Rodin, covers more of the standard rules, and adds interactive visualisation, HTML export, and replay to Rodin. The paper also reports a preliminary automatic prover using iterative deepening with simple heuristics, which already finds short proofs.

Load-bearing premise

The central assumption is that the Prolog clauses faithfully implement the mathematical proof rules of Event-B, so that every transition sequence the tool accepts is a sound proof; in particular, the normalisation-and-sorting equality check in the HYP rule must never certify an invalid sequent.

Editorial extensions

If this is right

  • Proofs built in ProB can be exported as Rodin BPR files and replayed in Rodin, giving an independent second toolchain for discharging proof obligations.
  • The interactive HTML proof-tree export lets students inspect a proof in any browser, showing exactly which rule changed which part of the sequent, without needing Rodin.
  • Because proof steps are fine-grained, a saved trace can be replayed and adapted after small model changes, supporting proof repair and reuse across refinements.
  • The compact Prolog encoding makes adding new proof rules a matter of writing a small clause rather than a Java class, which should accelerate future extensions.
  • A first automatic prover using iterative deepening is already included, and the authors expect partial evaluation to produce a very fast rule-based prover.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The special equality handling in the HYP rule — normalising terms into lists and comparing by sorting — is only sound if the sort order and normalisation respect the intended equational theory; a formal soundness proof or a large test suite would be needed to rule out subtle unsound cases.
  • Because the prover exposes individual rule applications, it could serve as a bridge for translating Event-B proofs into other proof frameworks, solving problems Rodin's coarse-grained 'simplification rewrites' cause for systems like TLAPS or Dedukti.
  • The iterative-deepening auto-prover currently has simple heuristics; applying partial evaluation or more sophisticated search strategies, as the authors suggest, could plausibly make this Prolog prover faster than Atelier-B's current engine.
  • The step-by-step interaction model, like the teaching-game approaches the authors cite, may significantly lower the barrier for students learning proof construction, but that pedagogical benefit is asserted from experience rather than measured.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper presents a Prolog implementation of Event-B sequent proof rules, integrated into the ProB tool via XTL. The system supports interactive proof construction, proof-tree visualization, HTML export, export to Rodin BPR files for replay, and a preliminary automated prover. The authors claim coverage of over 600 proof rules, a more compact encoding than Rodin's Java implementation (roughly an order of magnitude in LOC), and easier extensibility. The paper includes a worked example, a comparison table, and links to source code.

Significance. If the implementation is sound, this is a valuable contribution to the Event-B tool ecosystem: it provides a student-friendly interactive prover, a potential second proof chain, and a compact executable encoding of the proof rules that is easier to maintain than the Java code. The availability of source code and the use of ProB's existing infrastructure are strengths. However, the paper does not establish the soundness of the encoded rules, which is the central correctness property for a prover, and the Rodin replay validation is weaker than claimed because many steps are marked 'reviewed' rather than independently verified.

major comments (2)
  1. [Section 4, axiom(hyp) / member_hyps] The HYP rule as implemented is not the syntactic rule H,P ⊢ P. The text states that terms are normalised into special lists, compared by sorting, and that 'hypotheses may be stronger than the goal', e.g. y < x ⊢ x ≥ y. This is a semantic entailment, not ordinary HYP. No soundness proof, test suite, or independent checker is supplied for the normalisation or the 'stronger-than' relation. Since every closed branch can end in HYP, one over-permissive clause would invalidate proofs, HTML exports, and Rodin BPR files. Please add a proof that the normalisation and ordering preserve logical consequence (or are contained in it), or a systematic validation (e.g., random tests against Rodin or a trusted solver) covering the AC-normalisation and the arithmetic inequalities used by member_hyps.
  2. [Section 5.3, Export for Replay with Rodin] The abstract and introduction claim that proofs can be 'double-checked' in Rodin, but the mapping marks many automatic rewrite rules and custom rules as 'reviewed' steps, which Rodin replays without verifying them. Thus the BPR export inherits ProB's encoding for those steps and does not provide independent validation. Please quantify which rules are genuinely replayed by Rodin reasoners, make explicit that 'reviewed' means trusted from ProB, and adjust the 'second chain' claim accordingly.
minor comments (5)
  1. [Figure 2] The figure text contains a garbled repetition: 'radiation∈Z×Z 7 →Z∈Z×Z 7 →Z∈Z×Z 7 →Z' appears multiple times; this makes the example harder to follow.
  2. [Listing 3] The clause simp_rule(not_equal(L,L),falsity,...) rewrites L≠L to false without an explicit well-definedness side condition. Under Event-B's partial functions, L≠L may require WD(L); please clarify whether WD conditions are always separately guaranteed.
  3. [Section 4] The two uses of 'member' in member(member(R,RType),Hyps) are confusing; consider using a distinct predicate or a short comment for the AST membership.
  4. [Section 5.4] The claim that the auto-prover is 'already useful' for finding short proofs is not supported by any runtime or success-rate data. A few example timings or a small benchmark would make this concrete.
  5. [General] The paper mentions 'more than 600 proof rules' but Table 1 shows 4 rewrite and 8 inference rules are missing. State the total number explicitly and list the missing rules in an appendix.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: the paper is a tool-building and code-comparison report; self-citations to ProB infrastructure are minor and not load-bearing, and the stated soundness/verification limitations are correctness risks, not circularity.

full rationale

The paper's central claims are implementational: it encodes over 600 Event-B proof rules in Prolog, integrates them into ProB, and compares compactness and coverage against Rodin's Java sequent prover. None of these claims is derived by fitting parameters or by defining a quantity in terms of the thing it predicts, so the core circularity patterns (self-definition, fitted input called prediction, uniqueness imported from authors, ansatz smuggled by citation, renaming) do not apply. The example proof of the mars-rover WD obligation is a hand-checkable illustration with concrete Prolog clauses (Listings 3-4) and complete BPR/HTML exports, giving the central claim external, code-level content. The paper does rely on ProB infrastructure (XTL, WD prover, Graphviz interface) developed by the same group, with citations such as [16,22]; this is a normal tool dependency, and the proof-rule encodings are new and inspectable in the released source. The paper also explicitly flags its own limitations: Section 5.3 states that many automatic rewrite rules 'generate individual proof steps that are marked as "reviewed" ... enabling unverified replay in Rodin', and Section 4 admits that HYP is extended to 'hypotheses may be stronger than the goal' (y < x ⊢ x ≥ y). These are exactly the load-bearing soundness assumptions a correctness reviewer would focus on, and the absence of a machine-checked soundness proof or exhaustive test suite is a real correctness risk. But an unverified semantic rule is not a step that reduces by construction to its input; it is a potential bug or missing proof obligation, not circularity. The comparison with Rodin is an external benchmark and the development-effort claims are transparent. Hence no circular step can be exhibited, and the appropriate score is 2 at most, reflecting only minor self-citation to the authors' own ProB/WD-prover infrastructure.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper makes an engineering claim rather than a new mathematical claim. No free parameters are fitted to data. The ledger therefore consists of trust assumptions about the soundness of the encoded rules, the correctness of the Prolog encoding, and the correctness of supporting ProB infrastructure. The absence of a formal soundness proof is the main gap.

assumptions (5)
  • domain assumption The Event-B proof rules as defined by Abrial and Rodin are sound.
    The whole prover inherits its trustworthiness from the sequent-calculus rules it encodes. The paper cites Abrial and the Rodin rule wiki but does not prove the rules sound. Invoked throughout Section 2 and Section 4.
  • domain assumption Each Prolog clause exactly implements its corresponding mathematical rule, including the custom normalisation for associative-commutative operators and the 'stronger hypothesis' matching in HYP.
    Section 4 explains that plain Prolog unification is insufficient and that member_hyps normalises ground terms and sorts them. The paper provides no formal proof or exhaustive test that this encoding preserves soundness. This is the main implementation-specific premise.
  • domain assumption ProB's WD prover and the external provers used for side conditions (e.g., Z3, Atelier-B) are correct when used for well-definedness checks.
    Section 4, 'Rules with User Input', relies on ProB's WD analyser to compute WD(E). Incorrect WD analysis could permit unsound instantiations. This is an external component from the same authors, cited as [22].
  • domain assumption The XTL transition-system layer faithfully represents proof-rule applications as state transitions.
    The proof system is modelled as trans(Label,StateBefore,StateAfter). Soundness of the prover requires that any path in this transition system corresponds to a valid proof-tree derivation. The paper does not prove this correspondence; it is assumed by construction in Section 3 and Section 4.
  • standard math Gentzen sequent calculus and classical set theory provide the logical foundation of Event-B.
    Event-B is rooted in predicate logic and set theory; standard mathematical background. Used without proof, consistent with the field.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB." pith.science (2026). https://pith.science/paper/SSD7UJHR

@misc{pith2026260721191,
  author       = {Pith},
  title        = {Pith review of: Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SSD7UJHR}},
  note         = {Machine review of arXiv:2607.21191}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2607.21191 by the authors.

Figure 1
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], RODIN often applies sev￾eral proof steps simultaneously. The plugins of RODIN also conduct an en￾tire proof in a single step. In both cases, the user or student cannot easily check, understand or reproduce a proof.… view at source ↗
Figure 2
Figure 2. Application of Inference and Rewrite Rules to Prove a PO [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
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 new sequent prover animation mode, providing access to the proof transitions ( [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Visualisation of the Current and Previous Proof [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 6
Figure 6. 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. RODIN stores proof trees, along with the applied steps and the associated Java reaso…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

30 extracted references · 15 canonical work pages

  1. [1]

    Cambridge University Press

    Jean-Raymond Abrial (2005): The B-Book: Assigning Programs to Meanings. Cambridge University Press

    2005

  2. [2]

    Cambridge Univer- sity Press

    Jean-Raymond Abrial (2010): Modeling in Event-B: System and Software Engineering. Cambridge Univer- sity Press

    2010

  3. [3]

    Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta & Laurent V oisin (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

    doi:10.1007/s10009-010-0145-y 2010

  4. [4]

    Dedukti: a Logical Framework based on the $\lambda$$\Pi$-Calculus Modulo Theory

    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 . CoRR abs/2311.07185, doi:10.48550/ARXIV .2311.07185. arXiv:2311.07185

    work page Pith review arXiv doi:10.48550/arxiv.2311.07185 2023

  5. [5]

    Bernhard Beckert & Joachim Posegga (1995): leanTAP: Lean Tableau-based Deduction. J. Autom. Reason- ing 15(3), pp. 339–358, doi:10.1007/BF00881804

    doi:10.1007/bf00881804 1995

  6. [6]

    In: Proceedings FMICS, LNCS 12863, pp

    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, pp. 193–201, doi:10.1007/978-3-030-85248-1 12

    work page doi:10.1007/978-3-030-85248-1 2021

  7. [7]

    CoRR abs/2108.07878

    Christiano Braga & Narciso Mart ´ı-Oliet (2021): B Maude: A formal executable environment for Abstract Machine Notation Descriptions. CoRR abs/2108.07878. arXiv:2108.07878

    arXiv 2021

  8. [8]

    Butler & Issam Maamria (2013): Practical Theory Extension in Event-B

    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 , pp. 67–81, doi:10.1007/978-3-642-39698-4 5

    work page doi:10.1007/978-3-642-39698-4 2013

Show all 30 references
  1. [9]

    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, pp

    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, pp. 2–16. Available at https:...

    2010

  2. [10]

    Melvin Fitting (1998): leanTAP Revisited. J. Log. Comput. 8(1), pp. 33–47, doi:10.1093/logcom/8.1.33

    1998 doi

  3. [11]

    Gansner (2011): Drawing graphs with Graphviz

    Emden R. Gansner (2011): Drawing graphs with Graphviz. Technical Report

    2011

  4. [12]

    Gerhard Gentzen (1935): Untersuchungen ¨uber das logische Schließen. I. Mathematische Zeitschrift 39(1), pp. 176–210, doi:10.1007/BF01201353

    1935 doi

  5. [14]

    In: Proceedings ABZ, LNCS 15728, Springer, pp

    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-94533- 5 8

    2025 doi

  6. [15]

    In: 12th Rodin User and Developer Workshop

    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

    2025

  7. [16]

    In: Proceedings ICLP, EPTCS

    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

    2026

  8. [17]

    Acta Didactica Napocensia 3

    Maxim Hendriks, Cezary Kaliszyk, Femke van Raamsdonk & Freek Wiedijk (2010): Teaching logic using a state-of-the-art proof assistant. Acta Didactica Napocensia 3

    2010

  9. [18]

    Digital Experiences in Mathematics Education , pp

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

    2025 doi

  10. [19]

    Romanovsky (2016):Rodin Plat- form Why3 Plug-In

    Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah & Alexander B. Romanovsky (2016):Rodin Plat- form Why3 Plug-In. In: Proceedings ABZ 2016 , LNCS 9675, pp. 275–281, doi:10.1007/978-3-319-33600- 8 21. K. Engels, J. Gruteser, and M. Leuschel 147

    2016 doi

  11. [20]

    In: Proceedings SEFM 2015 , LNCS 9276, Springer, pp

    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-3- 319-22969-0 15

    2015 doi

  12. [21]

    In: Proceedings PPDP’2008, ACM Press, pp

    Michael Leuschel (2008): Declarative Programming for Verification: Lessons and Outlook. In: Proceedings PPDP’2008, ACM Press, pp. 1–7, doi:10.1145/1389449.1389450

    2008

  13. [22]

    In: Proceedings iFM 2020, LNCS 12546, Springer, pp

    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

    2020 doi

  14. [23]

    In: Proceedings VPT 2020, EPTCS 320, pp

    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

    2020 doi

  15. [24]

    In: Prolog: The Next 50 Y ears, LNCS 13900, Springer, pp

    Michael Leuschel (2023): ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. In: Prolog: The Next 50 Y ears, LNCS 13900, Springer, pp. 239–247, doi:10.1007/978-3-031-35254- 6 19

    2023 doi

  16. [25]

    Butler (2008): ProB: an automated analysis toolset for the B method

    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

    2008 doi

  17. [26]

    Journal of Symbolic Computation 8(1-2), pp

    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

    1989 doi

  18. [27]

    In: Proceedings NFM 2025 , LNCS 15682, pp

    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-93706- 4 16

    2025 doi

  19. [28]

    AI Commun

    Alexandre Riazanov & Andrei V oronkov (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

    2002

  20. [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

    2012 doi

  21. [30]

    Available at https://hal.science/hal-04398119

    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

    2024

  22. [31]

    In: Proceedings ABZ, LNCS 12071, Springer, pp

    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 sourc...

    2020 doi

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.