In Mathematica version 7, there was a big advance in logic support ("Boolean computations" is the official name). This was not further developed in version 8.0. So now we have a fairly robust support for propositional calculus, but not too much for predicate calculus.
To this end, it would help a lot if we had an internal function capable of transforming a formula (logic formula, I mean) into the Prenex normal form or, even better, into a Skolem normal form.
Is anybody aware of a 3rd party package which addresses this problem?