Yes, thanks for both answers. I forgot to look carefully at 'n_elt' since
Alt-Ergo, Z3 were well behaving. Now thanks Martin for pointing out difference
between theorem provers and SMT's.
-JJ-
Le 9 janv. 2014 à 22:34, clochard a écrit :
> Dear Jean-Jacques,
>
> To complete Andrei's answer, t
Dear Jean-Jacques,
To complete Andrei's answer, the difference here is between TPTP
(E-prover,Spass,...)
and SMT (alt-ergo,cvc3,cvc4,Z3,...) theorem provers. The TPTP provers
perform
proof search under quantifiers while SMT usually do not (universal
quantifiers are
instantiated using the exist
Dear Jean-Jacques,
Unless I'm missing something, the axiom "n_elt" implies that every
non-empty list is infinite (has the n-th element for any n), which leads to
a contradiction. So it's rather more surprising that the provers other than
E don't prove the program.
Best,
Andrei
On 9 January 2014
Dear Why3-Folks,
Happy New Year! Let 2014 be much fruitful for Why3!
I run Why3 version 0.82 and E-prover 1.6. Following assertions are proved by
E-prover !! Which looks to me (and Chen Ran) quite abnormal. It is not proved
by others provers,
Do we miss anything ? (BTW, I asked -- in previous
On 19/12/2013 13:50, Jean-Jacques Levy wrote:
Hi Why3 folks!
I found a strange behaviour in Why3 0.82. Look at following program. It seems
that 'inline' transformation does not work properly. Am I correct ? It seems
that 0.81 is better behaving.
Sorry for the late reply. I had tested your ex
