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

Alan Schmitt alan.schmitt at polytechnique.org
Wed Sep 19 15:17:38 CEST 2012


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



More information about the Why3-club mailing list