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

• URL: http://arxiv.org/abs/2607.21191v1
• Date: Thu, 23 Jul 2026 11:16:32 GMT
• Title: Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
• Abstract summary: Event-B is a formal method rooted in predicate logic and set theory.<n>We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction.<n>By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system with proof tree visualisation.
• Score: 0.2676349883103403
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Show Me The Money: An Exercise in Proof-Driven Software Understanding [1.678913049066618]
  We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book.<n>We produce artifacts that make it easy for code changes to be checked against established invariants.<n>This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.
  arXiv  Detail & Related papers  (2026-07-17T20:39:40Z)
• OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
  OProver is a unified framework for agentic formal iteration theorem proving in Lean 4.<n>It runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL.<n>OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.
  arXiv  Detail & Related papers  (2026-05-17T06:39:05Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
  arXiv  Detail & Related papers  (2026-03-13T01:33:20Z)
• PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
  We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4.<n>Key to our approach is reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code.<n>Our checker supports all VeriPB kernel rules, including cutting-planes and proof-by-contradiction subproofs.
  arXiv  Detail & Related papers  (2026-02-09T14:13:30Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
  We introduce Proofr, the first language model trained to simplify Lean proofs without requiring additional human supervision.<n>Provr is trained via expert iteration and reinforcement learning, using Lean to verify simplifications and provide training signal.<n>Provr substantially compresses proofs generated by state-of-the-art RL-trained provers on standard benchmarks.
  arXiv  Detail & Related papers  (2025-10-17T14:45:30Z)
• Hierarchical Attention Generates Better Proofs [8.676187819105298]
  We introduce textbfHierarchical Attention, a regularization method that aligns attention mechanisms with mathematical reasoning structures.<n>Our approach establishes a five-level hierarchy from foundational elements to high-level concepts, ensuring structured information flow in proof generation.
  arXiv  Detail & Related papers  (2025-04-27T10:35:05Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  We introduce LeanProgress, a method that predicts the progress in the proof.<n>Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1%.
  arXiv  Detail & Related papers  (2025-02-25T07:46:36Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  Two lines of approaches are adopted for complex reasoning with LLMs.<n>One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps.<n>The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers.<n>We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
  arXiv  Detail & Related papers  (2023-11-16T11:26:21Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge [0.0]
  We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant. Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
  arXiv  Detail & Related papers  (2020-12-20T18:15:12Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.