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

2026-07-23 · Katharina Engels, Jan Gruteser, Michael Leuschel arxiv

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 Abstract BibTeX arXiv:2607.21191

Code (0)

등록된 구현이 없습니다.

Animation, Verification and Visualisation of Prolog Transition Systems with ProB

2026-07-23 · Jan Gruteser, Michael Leuschel, Katharina Engels, Fabian Vu arxiv

ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its…

Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context

2020-02-28 · Ludovic Font, Sébastien Cyr, Philippe R. Richard, Michel Gagnon

When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be …

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

2024-11-02 · Liao Zhang, David M. Cerna, Cezary Kaliszyk

Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appr…

Automated Theorem Proving Inductive logic programming Mathematical Proofs Prediction

Case study: solving P-99 with LPTP and an LLM

2026-07-23 · Fred Mesnard, Thierry Marianne, Étienne Payet, Wim Vanhoof arxiv

Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By solved we mean: generate the Pro…

Prolog Technology Reinforcement Learning Prover

2020-04-15 · Zsolt Zombori, Josef Urban, Chad E. Brown

We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover…

Automated Theorem Proving reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)