D23 Rule-based Prover: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r |
imported>Im06r |
||
| Line 1: | Line 1: | ||
[[Category:D23_Deliverable]] | [[Category:D23_Deliverable]] | ||
==Overview== | ==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== | ==Motivations== | ||
Revision as of 17:10, 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:
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.
