The key to solving this kind of deduction is how to perform the disjunctive syllogism, i..e how get from A v B and ¬A to B, using disjunction elimination.
The idea is the following: There two cases to consider -- either A or B. Assume A. This leads to a contradiction with the second assumption ¬A, so we get ⊥. From a contradiction we may assume anything, so conveniently we can choose B. And the second case, B, is easy -- we already have our desired conclusion right there, we can just reiterate the assumption. Since from both cases we obtained B, and we know that at least one of the cases is true, we may conclude B for sure. This is disjunction elimination.
Formally, this looks as follows:
Now we just need to apply this technique to the disjunctions in your problem.
I can see why it has to be either A or D, because if it's B and C, then it cannot be ¬B or ¬C so it must be D.
First, let's figure out how to conclude from B and C that it cannot be ¬B or ¬C. So we need a subproof with premise B ^ C that has ¬(¬B ∨ ¬C) as its conclusion. We do not apply the disjuntive syllogism technique yet, ths is for later; instead, the idea is a proof by contradiction:
Assume that (¬B ∨ ¬C) does hold, and furthermore add B ^ C to the premise. There are two subproofs: 1. Assume ¬B. Form B ^ C we know B, which is a contradiction to ¬B, hence ⊥. 2. Analogous for ¬C. So from both disjuncts we get ⊥, and by disjunction elimination we are allowed to conclude ⊥. Since the assumption (¬B ∨ ¬C) led to a contradiction, we can apply negation introduction and get ¬(¬B ∨ ¬C), which we wanted because we can plug this in in the other proof.
Now we're in the state that we have ¬(¬B ∨ ¬C), and want to conclude D. This is where the disjunctive syllogism enters. ¬(¬B ∨ ¬C) is our ¬A from above, and ((¬B ∨ ¬C) v D) is A v B. So just insert these formulas into the schema from above, and we get
Plugging these two pieces together (the second proof is just a continuation of the first proof, which ended with ¬(¬B ∨ ¬C)), we got from B ^ C to D: We successfully proved
if it's B and C, then it cannot be ¬B or ¬C so it must be D.
| B ^ C
| ...
| ¬(¬B ∨ ¬C)
| ...
| D
Now we just need to justify the assumption B ^ C somehow, and get from D to A v D.
The above all happend under the assumption B ^ C. Now B ^ C is just one of the disjuncts in the premise A v (B ^ C). So to complete the proof, we make a second subproof which starts with A, and if we manage to conclude A v D from both cases, then we are allowed to apply a final disjunction elimination and proved A v B from the disjunction A v (B ^ C):
| A v (B ^ C)
| -------------
| | A
| | -----------
| | ...
| | A v D
|
| | B ^ C
| | -----------
| | ...
| | A v D
| A v D (vE)
So how to fill in the ...s?
In the subproof starting with assumption B ^ C, we already got D, so we can weaken this to A v D by a simple disjunction introduction.
And likewise, in the subproof starting with A, we already got A, so we can weaken this with a disjunction introduction on the other side to A v D.
And no we're done -- this is what the final proof looks like:
Using the schema shown above, maybe you can figure out the proof for the cube problem yourself?
