Rule-based Prover Plug-in

From Event-B
Revision as of 13:52, 1 December 2009 by imported>Im06r (→‎User Documentation)
Jump to navigationJump to search

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

News

  • 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|http://wiki.event-b.org/images/Theory_User_Manual.pdf].

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.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.