Rule-based Prover Plug-in: Difference between revisions

Revision as of 12:00, 1 December 2009

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

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

@@ Line 19: / Line 19: @@
 * Once rules are specified, only the validated ones are available. By validated, we mean "whose proof obligations are dischareg 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.