[Why3-club] simple propositional logic in why3 (with alt-ergo)

Mário José Parreira Pereira mariojppereira at gmail.com
Wed Sep 19 15:31:53 CEST 2012


Hello,

Which version of alt-ergo are you using? With alt-ergo 0.94 I was able 
to prove your goal.

It seems that, probably, it is a problem with the prover itself.

Best regards,
Mário
> Hello,
>
> For a course I'm teaching, I'm starting with very simple propositional
> logic. Here is an example of something I've written:
>
> theory TD1
>
>    predicate a
>    predicate b
>
>    goal G1 : (a /\ b) -> (b /\ a)
>
> end
>
> (I would have like to use A and B but it seems identifiers must start
> with a lower-case letter.)
>
> My problem is that alt-ergo is not able to solve this. I get an error
> like this:
>
> HighFailure (0.10s)
> Prover exit status: exited with status 127
> Prover output:
>
> Is it a problem with alt-ergo, with why3, or (more probably) with what I
> wrote?
>
> Thanks a lot,
>
> Alan
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club





More information about the Why3-club mailing list