# 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) ∨ (b ∧ c) == (a ∨ b) ∧ (a ∨ c)


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

(a) ∨ (b ∧ c) == (a ∨ b) ∧ (a ∨ c)


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

SatisfiabilityInstances[(a) ∨ (b ∧ c) == (a ∨
b) ∧ (a ∨ 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.

FindEquationalProof is available as an option:

booleanAxioms =
{ForAll[{a, b}, and[a, b] == and[b, a]],
ForAll[{a, b}, or[a, b] == or[b, a]],
ForAll[{a, b}, and[a, or[b, not[b]]] == a],
ForAll[{a, b}, or[a, and[b, not[b]]] == a],
ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]],
ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}
setOperationAxioms =
{ForAll[{a, b, x},
and[member[x, a], member[x, b]] == member[x, intersection[a, b]]],
ForAll[{a, b, x},
or[member[x, a], member[x, b]] == member[x, union[a, b]]]}
FindEquationalProof[
ForAll[{x, a, b, c},
member[x, union[a, intersection[b, c]]] ==
member[x, intersection[union[a, b], union[a, c]]]] ,
Union[booleanAxioms, setOperationAxioms]]