Clues on theorem proving tools?

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?

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

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

Equivalent is effectively Equal for Boolean expressions.