I would like to convert logical relational expressions in disjunctive form, e.g.,

$$(x \lt -1) \lor (-1 \lt x \lt +1) \lor (x \gt +1)$$

into conjunctive form, e.g.,

$$(x \ne -1) \land (x \ne +1)$$

I have some machinery in place that converts a logical relational expressions in disjunctive form into a union of intervals:


mxInterval::unrecognized = "The expression `` is not an Inequality, Less, LessEqual, GreaterEqual\
 or Greater operator or the logical Or of one or more of the operators.";                         

mxInterval[HoldPattern[Inequality[valueLeft_, ropLeft_, var_, ropRight_, valueRight_]]] :=        
    mxInterval[ropLeft, valueLeft, valueRight, ropRight];                                         

mxInterval[(rop:(Less|LessEqual))[var_, value_]] :=                                               
    mxInterval[LessEqual, "-∞", value, rop];                                            

mxInterval[(rop:(Greater|GreaterEqual))[var_, value_]] :=                                         
    mxInterval[rop, value, "∞", GreaterEqual];                                          

mxInterval[HoldPattern[Or[x__]]] :=                                                               
    Or @@ Replace[HoldComplete[x], elem_ :> mxInterval[elem], {1}];                               

mxInterval[expr_] := (Message[mxInterval::unrecognized, expr]; Return $fail;)                     

mxIntervalSymbol[op_, side_] := Switch[                                                           
    Less|Greater, Switch[side, l, "[", r, "]"],                                                   
    LessEqual|GreaterEqual, Switch[side, l, "(", r, ")"]];                                        

mxInterval /: MakeBoxes[mxInterval[ropLeft : (Less|LessEqual|Greater|GreaterEqual),               
                               valueLeft_, valueRight_,                                       
                               ropRight : (Less|LessEqual|Greater|GreaterEqual)], form_] :=   
    RowBox[{mxIntervalSymbol[ropLeft, l], MakeBoxes[valueLeft, form], ",",                        
            MakeBoxes[valueRight, form], mxIntervalSymbol[ropRight, r]}];   

Using mxInterval on the sample expression produces a disjunction of intervals,

In[]: mxInterval[x < -1 || -1 < x < +1 || x > +1]

Out[]: Or[mxInterval[-∞,LessEqual,Less,-1],

which display as:

$$(-\infty, -1] \cup [-1,+1] \cup [+1,+\infty)$$

or, as the number line: oops, which is actually of $(-\infty,-1] \cup [+1,+1\infty)$:


(Note: Maybe I should produce Union instead of Or here. Would that eliminate the needs for a MakeBoxes definition for Or[mxInterval ..]? The only use for that function is to get the $\cup$ operator instead of $\lor$ in the display).

What I would really like is the function mxInterval[Or[mxInterval ..], And] which would take the disjunctive form of intervals and produce the conjunctive form. And, of course, mxInterval[And[mxInterval ..], Or] that would do the reverse.

If I were using a more procedural language, I would sort and then iterate over the intervals constructing the result along the way. However, I feel like the best way to implement the function in Mathematica is to rely heavily on pattern matching, but I'm having trouble formulating a solution using that paradigm.

Or, maybe there is a Mathematica incantation that will do the conversion on the original logical relational expression? That would be sweet.

  • 3
    $\begingroup$ This works for your simple example. Might not generalize well though, I'm not sure. In[27]:= BooleanConvert[! Reduce[! ee], "CNF"] Out[27]= x != -1 && x != 1 $\endgroup$ – Daniel Lichtblau Mar 9 '13 at 20:06
  • $\begingroup$ That works for my current test cases, but BooleanConvert seems to ignore the form specification for "DNF" and "CNF": BooleanConvert[!Reduce[!result]] produces the same result as BooleanConvert[!Reduce[!result], "DNF"] and BooleanConvert[!Reduce[!result], "CNF"]. Specifying "NAND" and "NOR" does produce the expected results. I'd like to try to understand why this produces the CNF form and add a few more test cases. $\endgroup$ – RandomBits Mar 9 '13 at 20:35
  • $\begingroup$ I suspect "DNF" is a default form. From the point of view of basic logic, a statement of the form a AND b with (a,b) both atomic is already in DNF, trivially, as an OR with but one clause. obviously it is also in CNF. This may explain the behavior you note. $\endgroup$ – Daniel Lichtblau Mar 9 '13 at 20:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.