Exercise 7.33

Suppose an agent inhabits a world with two states, $S$ and $\lnot S$, and can do exactly one of two actions, $a$ and $b$. Action $a$ does nothing and action $b$ flips from one state to the other. Let $S^t$ be the proposition that the agent is in state $S$ at time $t$, and let $a^t$ be the proposition that the agent does action $a$ at time $t$ (similarly for $b^t$).

1. Write a successor-state axiom for $S^{t+1}$.

2. Convert the sentence in (a) into CNF.

3. Show a resolution refutation proof that if the agent is in $\lnot S$ at time $t$ and does $a$, it will still be in $\lnot S$ at time $t+1$.