# Prenex and Skolem normal forms

In MMA 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?

-
tutorial/RealPolynomialSystems claims "Reduce, Resolve, and FindInstance always put real polynomial systems in the prenex normal form, with quantifier-free parts in the disjunctive normal form"... –  Daniel Lichtblau Jan 20 '12 at 20:47
@DanielLichtblau this is a great suggestion Daniel, You may consider putting this as an answer –  magma Jan 21 '12 at 18:53

tutorial/RealPolynomialSystems claims "Reduce, Resolve, and FindInstance always put real polynomial systems in the prenex normal form, with quantifier-free parts in the disjunctive normal form..."

For obtaining Skolem form from prenex, possibly could proceed as described at

http://demonstrations.wolfram.com/Skolemization/

or

http://mathworld.wolfram.com/SkolemFunction.html

Edit:

Also there is a non-System context function of interest (I learned this via grep). I'll illustrate with the example provided in a comment.

ee = ForAll[x, P[x] \[Implies] Q[x]] \[Implies] (ForAll[x, P[x]] \[Implies] ForAll[x, Q[x]]);


We'll need to put into a normal for; conjunctive or disjunctive will suffice. I'll use LogicalExpand to get a dnf.

ff = LogicalExpand[ee]

Exists[x,  !Implies[P[x], Q[x]]] || Exists[x,  !P[x]] || ForAll[x, Q[x]]

ReduceToPrenexForm[ff]

Exists[{C[1], C[2]}, ForAll[{C[3]}, (P[C[1]] &&  !Q[C[1]]) ||  !P[C[2]] || Q[C[3]]]]


I've no idea whether this is the sort of result wanted. But it does seem to have all quantifiers at the front.

-
As I said above this is an excellent suggestion, but it does not really solve my problem. It seems that this transformation to prenex normal form, which takes place internally (probably with Resolve), is executed only on polynomial systems, not general first-order language formulas. For ex: ForAll[x, P[x] [Implies] Q[x]] [Implies] (ForAll[x, P[x]] [Implies] ForAll[x, Q[x]]) // Resolve does not do anything, because the expr is not in the form expected by MMA. Is there some undocumented function which can deal with this more general situation? –  magma Jan 24 '12 at 1:43
I am waiting a little bit to see if some other/better answer comes along, then I will accept one –  magma Jan 24 '12 at 16:14
@magma See edited post. –  Daniel Lichtblau Jan 24 '12 at 16:46
Great Daniel! This is exactly the result I was looking for. I do not understand why WRI keeps this function undocumented. It is very useful in ATP. But this will be the topic for another question –  magma Jan 24 '12 at 17:09
@magma It turns out we don't document this because prenex repositioning and skolemization are illegal activities in most southern states. (Did I really write that?) –  Daniel Lichtblau Jan 27 '12 at 23:26