This is documentation for Mathematica 8, which was
based on an earlier version of the Wolfram Language.

# Disjunction

 Disjunction gives the disjunction of expr over all choices of the Boolean variables .
• Disjunction applies Or to the results of substituting all possible combinations of True and False for the in expr.
The disjunction over a set of variables:
Check whether an expression is satisfiable:
Find the conditions on a for to be satisfiable:
The disjunction over a set of variables:
 Out[1]=

Check whether an expression is satisfiable:
 Out[1]=

Find the conditions on a for to be satisfiable:
 Out[1]=
Disjunction effectively computes the Or over all truth values of the listed variables:
Disjunction is typically more efficient and can work large numbers of variables:
Disjunction eliminates (Exists) quantifiers for the list of variables:
Use Resolve to eliminate more general combinations of quantifiers:
SatisfiableQ is Disjunction over all variables:
Use Conjunction to compute And over a list of variables:
Conjunction is related to Disjunction by de Morgan's law:
Disjunction is effectively repeated Or, just as Sum is repeated Plus:
Represent Disjunction in terms of Sum:
New in 7