Difference between revisions of "D23 Rule-based Prover"
From Event-B
Jump to navigationJump to searchimported>Im06r |
imported>Im06r |
||
| Line 5: | Line 5: | ||
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. | |
| − | + | *Prover Extension: which is reponsible for checking what rules are applicable and applying them. | |
==Motivations== | ==Motivations== | ||
Revision as of 17:11, 26 November 2009
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:
- The Theory construct: where rules are defined and validated by means of proof obligations.
- Prover Extension: which is reponsible for checking what rules are applicable and applying them.
