Take the 2-minute tour ×
Mathematica Stack Exchange is a question and answer site for users of Mathematica. It's 100% free, no registration required.

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?

share|improve this question
2  
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
add comment

1 Answer

up vote 7 down vote accepted

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]]
Reduce`ToPrenexForm[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.

share|improve this answer
    
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
show 5 more comments

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.