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