Hello,
I want to get a problem in TPTP format from a task expressed in Why3. Is
there already a way to do this, either with Why3 or another tool?
Ideally, I would do this through the API for OCaml, but I will take
anything. Thanks in advance.
Antoine Defourné
Hello,
You should decide which TPTP format, e.g
why3 prove -D tptp-tff0 file.why
or
why3 prove -D tptp-tff1 file.why
- Claude
Le 10/05/2017 à 11:32, Antoine DEFOURNE a écrit :
> Hello,
>
> I want to get a problem in TPTP format from a task expressed in Why3. Is
> there already a way to do