10
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ 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"... $\endgroup$
    – Daniel Lichtblau
    Jan 20, 2012 at 20:47
  • $\begingroup$ @DanielLichtblau this is a great suggestion Daniel, You may consider putting this as an answer $\endgroup$
    – magma
    Jan 21, 2012 at 18:53

1 Answer 1

Reset to default
11
$\begingroup$

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.

Improve this answer
$\endgroup$
9
  • $\begingroup$ 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? $\endgroup$
    – magma
    Jan 24, 2012 at 1:43
  • $\begingroup$ @magma See edited post. $\endgroup$
    – Daniel Lichtblau
    Jan 24, 2012 at 16:46
  • $\begingroup$ 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 $\endgroup$
    – magma
    Jan 24, 2012 at 17:09
  • $\begingroup$ @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?) $\endgroup$
    – Daniel Lichtblau
    Jan 27, 2012 at 23:26
  • 1
    $\begingroup$ @Magma Yes, I agree maybe that remark was a bit too cryptic. What I meant was that, having access to the source files (and working on a Linux desktop), I used grep on them to learn that a ToPrenexForm function existed. I do not know if this would work with the .mx files that come with the Mathematica distribution (I do not know the extent to which things might be encrypted therein; possibly not at all). $\endgroup$
    – Daniel Lichtblau
    Jan 31, 2012 at 17:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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