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 ------------------------------------------