[Why3-club] Why3-club Digest, Vol 95, Issue 7

Sandrine Blazy Sandrine.Blazy at irisa.fr
Fri Mar 29 14:56:29 CET 2019


Dear Claude,

> Le 15 nov. 2018 à 12:01, why3-club-request at lists.gforge.inria.fr a écrit :
> 
> Since Why3 1.0 we wanted to disencourage users to intentionally choose a 
> particular prover to discharge a goal. We want to encourage instead the 
> use of the shortcut "0" "1" and "2" that selects a "strategy" which will 
> try several provers.
> 
> In essence, for begineers we suggest to try first "0", if it fails use 
> "s" to split, then "0" again on subgoals. Then on each specific unproved 
> subgoals, an option is to try "1" or "2 ».

Thanks for the advice; we asked our students to follow this strategy which 
worked very well until now.
However, the proof window shows that  "s" calls the transformation
split_vc, and strategy   « 1 » uses the transformation split_all_full.

What is the difference between both transformations, and when should I try
to split again instead of using strategy 1 ? Indeed, on some examples, 
« 1 » followed by « 2 » does not help, but splitting again followed by « 0 » 
is enough to prove the VCs.

Sandrine

> - Claude
> 
> Le 14/11/2018 à 18:55, Sandrine Blazy a écrit :
>> Hello,
>> 
>> In my why3 IDE, there is no keyboard shortcut for my installed provers.
>> Instead of a shortcut, I see « VoidSymbol » for each of my provers.
>> Is there a way to define a shortcut for a given prover ?

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190329/e6444e2f/attachment.html>


More information about the Why3-club mailing list