Proof of simple conditional logic with resolution

Question

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?

Answer 1

We have to write down all the clauses corresponding to the premises, with the negation of the sought conclusion.

If the conclusion is "that two red lights cannot be on simultaneously", we can formalize it as :

$\lnot (R_1 \land R_2)$.

There are four clauses produced from the second premise:

1) $¬G_1 ∨ ¬Y_1$

2) $¬G_1 ∨ ¬ R_1$

3) $¬Y_1 ∨ ¬R_1$

4) $G_1 ∨ Y_1 ∨ R_1$

and the same : 5)-8) for $i=2$.

From the other premise we have : $R_1 \to (G_2 ∨ Y_2)$ i.e.

9) $¬R_1 ∨ G_2 ∨ Y_2$

and : $¬(G_2 ∨ Y_2) ∨ R_1$ i.e.

10) $¬G_2 ∨ R_1$

11) $¬Y_2 ∨ R_1$

and the same : 12)-14) for $i=2$.

Finally, we have to add the negation of the conclusion:

15) $R_1$

16) $R_2$.

Finally, we apply the resolution procedure.

Answer 2

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. $$