D23 Rule-based Prover

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

Overview

The rule-based prover plug-in offers a uniform mechanism to define and validate proof rules which can then be used in proofs.

The rule-based prover plug-in has two important components:

  • The Theory construct: where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether it should be applied automatically, interactively or both.
  • Prover Extension: which is responsible for checking what rules are applicable and applying them.

The plug-in supports the definition and validation of rewrite rules. It is expected that the plug-in will also support defining inference rules.

The University of Southampton was responsible for the development of the rule-based prover.

Motivations

Choices/Decisions

Available Documentation

Planning