How do I move from the $5$ NAND-gate xor solution to the $4$ NAND-gate xor solution? When trying to make boolean functions out of logic gates, I tried to make the NAND ($\uparrow$) equivalent for the XOR function: $(a \land \lnot b) \lor (\lnot a \land b)$
$$\begin{align}
(a \land \lnot b) \lor (\lnot a \land b) \\
\lnot(a \land \lnot b) \land \lnot(\lnot a \land b) \\
(a \land \lnot b) \uparrow (\lnot a \land b) \\
(\lnot a \uparrow b) \uparrow (a \uparrow \lnot b) \\
((a \uparrow a) \uparrow b) \uparrow (a \uparrow (b \uparrow b))
\end{align}$$
This last expression uses all NANDs and requires five gates. However as it turns out there is an even shorter solution using four NAND gates:
$$(a \uparrow (a \uparrow b)) \uparrow ((a \uparrow b) \uparrow b)$$
Is there a way to get there naturally or is it just a clever solution you have to find by trial and error? Is there a way to get there mechanically? It appears the main advantage of this equation is the re-use of $(a \uparrow b)$ so there may be some "creative" element to it but I am asking in case there is some algorithmic or direct way to arrive at such a solution without needing to be clever.
 A: First of all, your own derivation is incorrect:

$$\begin{align}
(a \land \lnot b) \lor (\lnot a \land b) \\
\lnot(a \land \lnot b) \land \lnot(\lnot a \land b)  \\ 
(a \land \lnot b) \uparrow (\lnot a \land b) \\
(\lnot a \uparrow b) \uparrow (a \uparrow \lnot b) \\
((a \uparrow a) \uparrow b) \uparrow (a \uparrow (b \uparrow b))
\end{align}$$

Two mistakes:
First: the second line should be $ \lnot ((a \land \lnot b) \land \lnot(\lnot a \land b))$
Second: from line 2 to 3, as well as from 3 to 4, you are using $P \uparrow Q = \neg P \land \neg Q$, but we have $P \uparrow Q = \neg (P \land Q)$ instead.
So, even though it ends up being the same you have, the correct derivation is:
$$\begin{align}
(a \land \lnot b) \lor (\lnot a \land b) \\
\neg (\lnot(a \land \lnot b) \land \lnot(\lnot a \land b))  \\ 
\neg (a \land \lnot b) \uparrow \neg (\lnot a \land b) \\
(a \uparrow \neg b) \uparrow (\neg a \uparrow b) \\
(a \uparrow (b \uparrow b)) \uparrow ((a \uparrow a) \uparrow b)
\end{align}$$
OK, but how can we get to $(a \uparrow (a \uparrow b)) \uparrow ((a \uparrow b) \uparrow b)$?
Well, the Reduction principle says:
Reduction
$P \land (P \lor Q) = P \land Q$
That is, in the context of $P$, the $P \lor Q$ term 'reduces to just $Q$
Because the NAND is a disjunction in disguise, there will be a reduction principle here as well, but because of the negation, it turns out to be a little different:
Reduction for NAND
$P \land (P \uparrow Q) = P \land \neg Q$
From this, it now follows that:
$\neg (P \land (P \uparrow Q)) = \neg (P \land \neg Q)$
i.e. that:
$P \uparrow (P \uparrow Q) = P \uparrow \neg Q$
And that's the key equivalence, for notice that from the second to last line of the correct derivation:
$(a \uparrow \neg b) \uparrow (\neg a \uparrow b)=$
we can apply the above equivalence to immediately get:
$(a \uparrow (a \uparrow b)) \uparrow ((a \uparrow b) \uparrow b)$
Now ... was this a 'natural' way of getting to the answer? ... one that doesn't require one to be 'clever'? ... not really, right?  That is, you really would know the Reduction for NAND principle, and even then it takes a few non-obvious steps.  And that's the problem with the NAND: we're just not very practiced with the NAND, and the algebraic principles that hold for it just aren't as 'nice' as those for the $\lor$ and $\land$.  So, unless you do a lot more problems involving the NAND like this, it's never going to feel 'natural'. 
