Proof of simple conditional logic with resolution I have a problem where there are two traffic lights in a junction. If the red light $R_i$ in traffic light $i=1,2$ is on, then green either $R$ or yellow $Y$ is on the other light and vice versa. I think this can be expressed as
$$(R_1 \leftrightarrow (G_2 \lor Y_2)) \land (R_2 \leftrightarrow(G_1 \lor Y_1))$$
Also we need to enforce that two lights cannot be on simultaneously and one light exactly is on at each time,
\begin{align}\neg (G_i \land Y_i)\land \neg(G_i \land R_i) \land \neg (Y_i \land R_i)\land(G_i\lor Y_i \lor R_i)\end{align}
How would one proof with resolution that two red lights cannot be on simultaneously? 
Obviously if $R_i=1$, then either $G_{i^\prime}$ or $Y_{i^\prime}$ is 1 ($i^\prime = 1$ if $i = 2$ and vice versa) because otherwise $R_i \leftrightarrow (G_{i^\prime} \lor Y_{i^\prime}) =0$. Thus because $G_{i^\prime}$ or $Y_{i^\prime}$ is 1, $R_{i^\prime}$ cannot be 1 simultaneously because we would violate the clauses that exactly one light is on (To be more specific either $\neg(G_i \land R_i) \land \neg (Y_i \lor R_i)=0$). It seems clear cut, but I cannot formulate the formal resolution proof. Any help?

While @MauroALLEGRANZA has given the systematic solution, let me show a shortcut I'd use if I were to solve this problem with paper and pencil.  These three clauses, which are part of your assumptions,
$$(\neg G_i \vee \neg R_i) \wedge (\neg Y_i \vee \neg R_i) \wedge (G_i \vee Y_i \vee R_i)$$
are easily verified to be the CNF equivalent of $(G_i \vee Y_i) \leftrightarrow (\neg R_i)$.  By transitivity of equivalence you are done:
$$ R_i \leftrightarrow (G_{3-i} \vee Y_{3-i}) \leftrightarrow (\neg R_{3-i}) ~~~\text{ for } i \in \{1,2\} \enspace.$$
As an aside, real traffic lights may have simultaneous red lights for both intersecting roads, because the actual safety requirement they have to satisfy is the weaker
$$ (G_{3-i} \vee Y_{3-i}) \rightarrow R_i ~~~\text{ for } i \in \{1,2\} \enspace. $$
