Write an ML program for checking the tatuology of a given propositional formula.

Use the following datatype definition for writing the formulas:

            datatype prop =
                       Atom of string
                     | Neg   of  prop
                     | Conj  of  prop * prop
                     | Disj   of  prop * prop;

For example a boolean formula:

  p & ~p

will be represented as:

     Conj (Atom "p", Neg (Atom "p"))

The function to be called should have the following prototype definition:

   taut:prop->bool