Menu
▾
▴
#217 Prover not picking out contradiction in context
Hi,
In a context machine i have the following axioms:
axm1 aValue : MYSET >->> NAT1
axm2 0 : dom(aValue~)
infortunatly the proovers dont say thats somethings wrong with the second axiom, instead they 'giveup', giving The follwing PO pattern in the machine:
X|X, 0|0, 0
where X is the number of PO's in the machine.
The proovers should pick this problem out:(
In event-B, axioms are just given, so there is no consistency check provided by the tools. In your example, you have a contradiction between the two axioms, which could lead to have any model using these axioms being fully proved whatever its contents.
We know that this problem of contradiction in axioms is currently very difficult to detect. Our plans in the Deploy project is to provide means for instantiating a context, thus providing a model of it. This will allow users to ensure that axioms are not contradictory, if the provided model is simple enough.