Difference between revisions of "Improved WD Lemma Generation"
From Event-B
Jump to navigationJump to searchimported>Desaperh m |
imported>Desaperh m |
||
Line 10: | Line 10: | ||
The well-definedness lemma generated for predicate <math> x \div y=5 \land \lnot x \div y=3 </math> is | The well-definedness lemma generated for predicate <math> x \div y=5 \land \lnot x \div y=3 </math> is | ||
− | <math> \lnot y=0 \land (x\div y=5 \limp \lnot y=0) </math> | + | <math> \lnot y=0 \land (x\div y=5 \limp \lnot y=0) </math> |
+ | This predicate is sub-optimal as the sub-predicate <math> x\div y=5 \limp \lnot y=0 </math> is subsumed by the sub-predicate <math> \lnot y=0 </math>. The prover doesn't need to prove <math> x\div y=5 \limp \lnot y=0 </math> if <math> \lnot y=0 </math> has been proved. | ||
+ | |||
+ | The well-definedness lemma generated for predicate <math> \exists x.x=a\div b </math> is | ||
+ | |||
+ | <math> \forall x.\lnot b </math> | ||
+ | |||
+ | This predicate is sub-optimal as <math> \forall x </math> is unneccesary. | ||
+ | |||
[[Category:Developer documentation]] | [[Category:Developer documentation]] |
Revision as of 11:40, 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.
The well-definedness lemma generated for predicate is
This predicate is sub-optimal as the sub-predicate is subsumed by the sub-predicate . The prover doesn't need to prove if has been proved.
The well-definedness lemma generated for predicate is
This predicate is sub-optimal as is unneccesary.