[Why3-club] permut fix

Jean-Jacques Levy jean-jacques.levy at inria.fr
Wed Mar 12 08:19:42 CET 2014

Hi Guillaume!

Le 12 mars 2014 à 14:38, Guillaume Melquiond <guillaume.melquiond at inria.fr> a écrit :

> We prove it relatively to the consistency of Coq, that is, if Coq is consistent, then Why3 theories are consistent too. All the axions and lemmas of Why3 are translated to Coq statements, then proved in Coq. If it was possible to deduce False from Why3 theories in FOL, one could build a proof of False in Coq. So, by contraposition, we have relative consistency.

‘axioms of Why3 translated to Coq statements, then proved in Coq’!! It means that these axioms have other def in Coq ?? So you define a model starting from what ? I understand that you prove Lemmas. But axioms ?? Furthermore, I’d like you show how you prove in Coq that False cannot be derived !!!! I think you meant that if you have a consistent model, False cannot be proved.

Cheers, -JJ-

More information about the Why3-club mailing list