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 f(x) = f(y) is

f\in S\pfun T\land x\in\dom(f)\land f\in S\pfun T\land y\in\dom(f)

This predicate is sub-optimal as it contains twice the same sub-predicate (f\in S\pfun T). 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  x \div y=5 \land \lnot x \div y=3 is

 \lnot y=0 \land (x\div y=5 \limp \lnot y=0)  

This predicate is sub-optimal as the sub-predicate  x\div y=5 \limp \lnot y=0 is subsumed by the sub-predicate  \lnot y=0 . The prover doesn't need to prove  x\div y=5 \limp \lnot y=0 if  \lnot y=0 has been proved.


The well-definedness lemma generated for predicate  \exists x.x=a\div b is

 \forall x.\lnot b 

This predicate is sub-optimal as  \forall x is unneccesary.