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?

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

2 Answers 2

Reset to default
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.

Improve this answer
$\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]]
Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.