D23 Rule-based Prover
From Event-B
Overview
The rule-based prover plug-in offers a uniform mechanism to defined and validate proof rules.
The rule-based prover plug-in has two important components:
1) The Theory construct: where rules are defined and validated by means of proof obligations. 2) Prover Extension: which is reponsible for checking what rules are applicable and applying them.