Difference between revisions of "Improved WD Lemma Generation"
From Event-B
Jump to navigationJump to searchimported>Laurent (Added first motivating example) |
(No difference)
|
Revision as of 09:45, 21 April 2010
This page describes work in progress for optimising well-definedness lemmas generated by the Core Rodin platform.
Motivating examples
With Rodin 1.3, the well-definedness lemma generated for predicate is
This predicate is sub-optimal as it contains twice the same sub-predicate (). Consequently, when the prover is fed with the generated lemma, it will have to prove twice the same goal.