Theory Plug-in: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r No edit summary |
imported>Im06r |
||
Line 12: | Line 12: | ||
===Insider Look=== | ===Insider Look=== | ||
:[http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.] | |||
:[http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.] | |||
===Improvements and Bugs=== | ===Improvements and Bugs=== | ||
See also the late [[Rule-based Prover Plug-in]], the last release of the which was v0.3. The Theory plug-in starts at version v0.5. | See also the late [[Rule-based Prover Plug-in]], the last release of the which was v0.3. The Theory plug-in starts at version v0.5. |
Revision as of 11:42, 23 October 2010
Return to Rodin Plug-ins
The Theory plug-in is the successor of the Rule-based Prover (which will be referred to as RbP) plug-in. The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. If you are looking for the user manual or the latest news on the Theory plug-in, please refer to Theory News and Support. This page provides useful information about the plug-in and its design.
Motivation
Overview
Capabilities
Insider Look
- Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.
- Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.
Improvements and Bugs
See also the late Rule-based Prover Plug-in, the last release of the which was v0.3. The Theory plug-in starts at version v0.5.