Improved WD Lemma Generation: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Desaperh mNo edit summary |
imported>Desaperh mNo edit summary |
||
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.