11
$\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) ∨ (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?

$\endgroup$
2
  • $\begingroup$ Try Resolve and SameQ. $\endgroup$
    – IPoiler
    Jan 26, 2016 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$ Jan 26, 2016 at 15:32

2 Answers 2

6
$\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$
4
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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