[Haskell-beginners] Formal proof with haskell

[Sebastien Lannez]

Dear all,

I am currenlty learning Haskell.

I want to use it to solve combinatorial problems.

I want Haskell to prove a simple logical assertion (a tautology) ...
Unfortunately, I failed to express it in Haskell.

The logical proposition:
proof1 x z = ( (not (x<z)) || ( (x<y) && (y<z) )
                    where y = (x+z)/2

It is easy to see that simple substitution lead to
proof1 x z = (not (x<z)) || (x<z) = True

Is Haskell smart enough to automatically solve such tautology ?

------------------------------------------
Sébastien Lannez
Expert Optimisation
------------------------------------------
www: http://www.lannez.fr
tel. (home): +33 9 81 16 50 74
tel. (office): +33 1 64 47 85 73
mob.: +33 6 31 82 32 19
------------------------------------------