Rule-based Prover Plug-in: Difference between revisions

Revision as of 11:58, 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.

@@ Line 10: / Line 10: @@
 ''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.