Rule-based Prover Plug-in
From Event-B
This page provides extensive documentation for the rule-based prover plug-in.
News
- 8th February 2009: Version 0.2.0 released. It is based on Rodin 1.2.0.
- 1st December 2009: Version 0.0.1 released. It is based on Rodin 1.1.0.
Installation & Update
The installation or update for the theory/rule-based prover plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates). Like always, after the installation, restarting Rodin is recommended.
User Documentation
The user manual is available here.
Other Documentation
- Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.
- Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, Technical Report.
Bugs & Problems
Releases
Version 0.2.0
8th February 2009
This release includes bug fixes, and added (partial) support for rules containing set extension (singleton).
Version 0.0.1
1st December 2009
This is the first public release of the Rule-based Prover plug-in (another name for this plug-in is Theory).
General:
- A theory construct is implemented to facilitate the specification and validation of rewrite rules.
- A pattern matching mechanism is implemented to check for applicability of rules as well as apply them.
- This is the first public release, so likely to have bugs. Use with care.
- Once rules are specified, only the validated ones are available. By validated, we mean "whose proof obligations are either dischared or reviewed".
- It is expected that Associative and Associative Commutative matching will have some issues. These will get rectified in the next release.
Limitations:
- This plug-in does not handle rules where the left hand side has a set extension.
- This plug-in should not be used to define rules with side conditions.
- Both these limitations will be addressed in future releases.
