8
$\begingroup$

I'm trying to prove $[a \cup (b \cap c ) = (a\cup b)\cap (a\cup c)]$ with Mathematica. But I don't know what function I should use. I've rewritten the sentence in the following way:

(a) \[Or] (b \[And] c) == (a \[Or] b) \[And] (a \[Or] c)

With $a$ being a symbol for $x\in a$ and the same for the other letters. I've just tried to evaluate:

(a) \[Or] (b \[And] c) == (a \[Or] b) \[And] (a \[Or] c)

but nothing happened. I've also tried to use:

SatisfiabilityInstances[(a) \[Or] (b \[And] c) == (a \[Or] 
  b) \[And] (a \[Or] c), {a, b, c}]

but I'm not sure I understand the output. I am aware of the BooleanTable, but I'd like to use some more advanced theorem proving tools in Mathematica. Could you give me a hint of where to go?

$\endgroup$
  • $\begingroup$ Try Resolve and SameQ. $\endgroup$ – IPoiler Jan 26 '16 at 15:11
  • $\begingroup$ BooleanTable[{a, b, c} -> Equal @@ {(a) \[Or] (b \[And] c), (a \[Or] b) \[And] (a \[Or] c)}, {a, b, c}] // Column $\endgroup$ – Dr. belisarius Jan 26 '16 at 15:32
3
$\begingroup$

You can compose TautologyQ and Equivalent

ClearAll[bEq]
bEq = TautologyQ @* Equivalent;

Examples:

bEq[a && (b || c), a && b || a && c] 

True

table = Table[BooleanConvert[BooleanFunction[30, {a, b, c}], form],
  {form, {"DNF", "CNF", "ANF", "NAND", "NOR", "ITE"}}]

{(a && ! b && ! c) || (! a && b) || (! a && c),
(! a || ! b) && (! a || ! c) && (a || b || c),
a ⊻ b ⊻ c ⊻ (b && c),
(a ⊼ ! b ⊼ ! c) ⊼ (! a ⊼ b) ⊼ (! a ⊼ c),
(! a ⊽ ! b) ⊽ (! a ⊽ ! c) ⊽ (a ⊽ b ⊽ c),
If[a, If[b, False, If[c, False, True]], If[b, True, If[c, True, False]]]}

bEq @ table

True

From Equivalent >> Properties and Relations:

Equivalent is effectively Equal for Boolean expressions.

$\endgroup$

Your Answer

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

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