Rule-based Prover Plug-in

This page provides extensive documentation for the rule-based prover plug-in.

News

• 8th February 2010: 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.

Releases

Version 0.2.0

8th February 2010

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.