D23 Rule-based Prover: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r |
imported>Im06r |
||
| Line 2: | Line 2: | ||
==Overview== | ==Overview== | ||
The rule-based prover plug-in offers a uniform mechanism to | The rule-based prover plug-in offers a uniform mechanism to define and validate proof rules. | ||
The rule-based prover plug-in has two important components: | The rule-based prover plug-in has two important components: | ||
*The Theory construct: where rules are defined and validated by means of proof obligations. | *The Theory construct: where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether a rule should be applied automatically, interactively or both. | ||
*Prover Extension: which is reponsible for checking what rules are applicable and applying them. | *Prover Extension: which is reponsible 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== | ==Motivations== | ||
Revision as of 17:17, 26 November 2009
Overview
The rule-based prover plug-in offers a uniform mechanism to define and validate proof rules.
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 a rule should be applied automatically, interactively or both.
- Prover Extension: which is reponsible 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.
