How does this boolean expression simplify? I was able to simplify a boolean expression $$(\neg a*\neg b*c)+(a*\neg b*\neg c)+(a*b*\neg c)+(a*b*c)$$into the form $$\neg b*(a\oplus c)+a*b$$ where $*$ is the logical and, $+$ is the logical or, and $\oplus$ is the logical XOR.
Apparently, from Wolfram Alpha, this expression can be simplified to $$\left(a\oplus c\right)\oplus(b*c)$$
I would like to know how Wolfram Alpha was able to simplify this.
 A: I'm not privy to the internals of Wolfram Alpha, but here's a way to derive the expression it produces.
First of all, it's not unreasonable to assume that if the input contains an exclusive OR, WA may decide that the user wants to see exclusive ORs in the output, or is at least OK with them.
Let $f = \neg b * (a \oplus c)  + (a * b)$.  Applying Reed-Muller expansion with respect to $b$, we get cofactors $f_b = a$, $f_{\neg b} = a \oplus c$, Boolean difference $\frac{\partial f}{\partial b} = c$, and hence
$$ f = f_{\neg b} \oplus b * \frac{\partial f}{\partial b} = (a \oplus c) \oplus (b * c) \enspace. $$
The choice of $b$ for the expansion is enticing when computing by hand because the cofactors and the Boolean difference are easy to find.  Is this what WA does?  Expansion w.r.t. $a$ produces
$$a \oplus (\neg b * c) \enspace. $$
Expansion w.r.t. $c$ also produces this result.  This expression is more concise than the previous one, but not in Reed-Muller canonical form, which may be what WA is shooting for.  Conversion produces
$$ a \oplus ((1 \oplus b) * c) = a \oplus c \oplus (b*c) \enspace. $$
So, no matter how we do the expansion, we end up with the expected result if we shoot for Reed-Muller canonical form.  The parentheses in the expression produced by WA suggest the expansion is actually carried out w.r.t. $b$. 
A: That expression you got from WA isn't the same as your original. It includes, for example, $(\neg a * b * \neg c)$, which is not included in your original expression. I figured that out by looking at a Venn diagram.

Edit: With that correction, WA's solution actually matches up. As for how they obtained it, I don't know what specific algorithm they use, but we can see that their expression is indeed equivalent to the original. It consists of two disjoint pieces: $(a\oplus c)*\neg(b*c)$, and $\neg(a\oplus c)*(b*c)$. The first piece is equivalent to $(a*\neg b*\neg c)+(a*b*\neg c)+(\neg a*\neg b*c)$, while the second is the same as $(a*b*c)$.
Again, this is probably easiest to see by drawing a Venn diagram.
