Clues on theorem proving tools?

Question

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?

Answer 1

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.

Answer 2

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]]