D23 Rule-based Prover

From Event-B
Revision as of 17:10, 26 November 2009 by imported>Im06r (→‎Overview)
Jump to navigationJump to search

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.

Motivations

Choices/Decisions

Available Documentation

Planning