# 7. Logical Agents

Suppose the agent has progressed to the point shown in
Figure wumpus-seq35-figure(a), page wumpus-seq35-figure,
having perceived nothing in [1,1], a breeze in [2,1], and a stench
in [1,2], and is now concerned with the contents of [1,3], [2,2],
and [3,1]. Each of these can contain a pit, and at most one can
contain a wumpus. Following the example of
Figure wumpus-entailment-figure, construct the set of
possible worlds. (You should find 32 of them.) Mark the worlds in which
the KB is true and those in which each of the following sentences is
true:

$\alpha_2$ = “There is no pit in [2,2].”

$\alpha_3$ = “There is a wumpus in [1,3].”

Hence show that ${KB} {\models}\alpha_2$ and
${KB} {\models}\alpha_3$.

(Adapted from Barwise+Etchemendy:1993 .) Given the following, can you prove that the unicorn is
mythical? How about magical? Horned?

Note: If the unicorn is mythical, then it is immortal, but if it is not
mythical, then it is a mortal mammal. If the unicorn is either
immortal or a mammal, then it is horned. The unicorn is magical if it
is horned.

Consider the problem of deciding whether a
propositional logic sentence is true in a given model.

1. Write a recursive algorithm PL-True?$ (s, m )$ that returns ${true}$ if and
only if the sentence $s$ is true in the model $m$ (where $m$ assigns
a truth value for every symbol in $s$). The algorithm should run in
time linear in the size of the sentence. (Alternatively, use a
version of this function from the online code repository.)

2. Give three examples of sentences that can be determined to be true
or false in a *partial* model that does not specify a
truth value for some of the symbols.

3. Show that the truth value (if any) of a sentence in a partial model
cannot be determined efficiently in general.

4. Modify your algorithm so that it can sometimes judge truth from
partial models, while retaining its recursive structure and linear
run time. Give three examples of sentences whose truth in a partial
model is *not* detected by your algorithm.

5. Investigate whether the modified algorithm makes $TT-Entails?$ more efficient.

Which of the following are correct?

1. ${False} \models {True}$.

2. ${True} \models {False}$.

3. $(A\land B) \models (A{\;\;{\Leftrightarrow}\;\;}B)$.

4. $A{\;\;{\Leftrightarrow}\;\;}B \models A \lor B$.

5. $A{\;\;{\Leftrightarrow}\;\;}B \models \lnot A \lor B$.

6. $(A\land B){\:\;{\Rightarrow}\:\;}C \models (A{\:\;{\Rightarrow}\:\;}C)\lor(B{\:\;{\Rightarrow}\:\;}C)$.

7. $(C\lor (\lnot A \land \lnot B)) \equiv ((A{\:\;{\Rightarrow}\:\;}C) \land (B {\:\;{\Rightarrow}\:\;}C))$.

8. $(A\lor B) \land (\lnot C\lor\lnot D\lor E) \models (A\lor B)$.

9. $(A\lor B) \land (\lnot C\lor\lnot D\lor E) \models (A\lor B) \land (\lnot D\lor E)$.

10. $(A\lor B) \land \lnot(A {\:\;{\Rightarrow}\:\;}B)$ is satisfiable.

11. $(A{\;\;{\Leftrightarrow}\;\;}B) \land (\lnot A \lor B)$
is satisfiable.

12. $(A{\;\;{\Leftrightarrow}\;\;}B) {\;\;{\Leftrightarrow}\;\;}C$ has
the same number of models as $(A{\;\;{\Leftrightarrow}\;\;}B)$ for
any fixed set of proposition symbols that includes $A$, $B$, $C$.

Which of the following are correct?

1. ${False} \models {True}$.

2. ${True} \models {False}$.

3. $(A\land B) \models (A{\;\;{\Leftrightarrow}\;\;}B)$.

4. $A{\;\;{\Leftrightarrow}\;\;}B \models A \lor B$.

5. $A{\;\;{\Leftrightarrow}\;\;}B \models \lnot A \lor B$.

6. $(A\lor B) \land (\lnot C\lor\lnot D\lor E) \models (A\lor B\lor C) \land (B\land C\land D{\:\;{\Rightarrow}\:\;}E)$.

7. $(A\lor B) \land (\lnot C\lor\lnot D\lor E) \models (A\lor B) \land (\lnot D\lor E)$.

8. $(A\lor B) \land \lnot(A {\:\;{\Rightarrow}\:\;}B)$ is satisfiable.

9. $(A\land B){\:\;{\Rightarrow}\:\;}C \models (A{\:\;{\Rightarrow}\:\;}C)\lor(B{\:\;{\Rightarrow}\:\;}C)$.

10. $(C\lor (\lnot A \land \lnot B)) \equiv ((A{\:\;{\Rightarrow}\:\;}C) \land (B {\:\;{\Rightarrow}\:\;}C))$.

11. $(A{\;\;{\Leftrightarrow}\;\;}B) \land (\lnot A \lor B)$
is satisfiable.

12. $(A{\;\;{\Leftrightarrow}\;\;}B) {\;\;{\Leftrightarrow}\;\;}C$ has
the same number of models as $(A{\;\;{\Leftrightarrow}\;\;}B)$ for
any fixed set of proposition symbols that includes $A$, $B$, $C$.

Prove each of the following assertions:

1. $\alpha$ is valid if and only if ${True}{\models}\alpha$.

2. For any $\alpha$, ${False}{\models}\alpha$.

3. $\alpha{\models}\beta$ if and only if the sentence
$(\alpha {\:\;{\Rightarrow}\:\;}\beta)$ is valid.

4. $\alpha \equiv \beta$ if and only if the sentence
$(\alpha{\;\;{\Leftrightarrow}\;\;}\beta)$ is valid.

5. $\alpha{\models}\beta$ if and only if the sentence
$(\alpha \land \lnot \beta)$ is unsatisfiable.

Prove, or find a counterexample to, each of the following assertions:

1. If $\alpha\models\gamma$ or $\beta\models\gamma$ (or both) then
$(\alpha\land \beta)\models\gamma$

2. If $(\alpha\land \beta)\models\gamma$ then $\alpha\models\gamma$ or
$\beta\models\gamma$ (or both).

3. If $\alpha\models (\beta \lor \gamma)$ then $\alpha \models \beta$
or $\alpha \models \gamma$ (or both).

Prove, or find a counterexample to, each of the following assertions:

1. If $\alpha\models\gamma$ or $\beta\models\gamma$ (or both) then
$(\alpha\land \beta)\models\gamma$

2. If $\alpha\models (\beta \land \gamma)$ then $\alpha \models \beta$
and $\alpha \models \gamma$.

3. If $\alpha\models (\beta \lor \gamma)$ then $\alpha \models \beta$
or $\alpha \models \gamma$ (or both).

Consider a vocabulary with only four propositions, $A$, $B$, $C$, and
$D$. How many models are there for the following sentences?

1. $B\lor C$.

2. $\lnot A\lor \lnot B \lor \lnot C \lor \lnot D$.

3. $(A{\:\;{\Rightarrow}\:\;}B) \land A \land \lnot B \land C \land D$.

We have defined four binary logical connectives.

1. Are there any others that might be useful?

2. How many binary connectives can there be?

3. Why are some of them not very useful?

Using a method of your choice, verify each of the equivalences in Table logical-equivalence-table (page logical-equivalence-table).

Decide whether each of the following
sentences is valid, unsatisfiable, or neither. Verify your decisions
using truth tables or the equivalence rules of
Table logical-equivalence-table (page logical-equivalence-table).
1. ${Smoke} {\:\;{\Rightarrow}\:\;}{Smoke}$

2. ${Smoke} {\:\;{\Rightarrow}\:\;}{Fire}$

3. $({Smoke} {\:\;{\Rightarrow}\:\;}{Fire}) {\:\;{\Rightarrow}\:\;}(\lnot {Smoke} {\:\;{\Rightarrow}\:\;}\lnot {Fire})$

4. ${Smoke} \lor {Fire} \lor \lnot {Fire}$

5. $(({Smoke} \land {Heat}) {\:\;{\Rightarrow}\:\;}{Fire})
{\;\;{\Leftrightarrow}\;\;}(({Smoke} {\:\;{\Rightarrow}\:\;}{Fire}) \lor ({Heat} {\:\;{\Rightarrow}\:\;}{Fire}))$

6. $({Smoke} {\:\;{\Rightarrow}\:\;}{Fire}) {\:\;{\Rightarrow}\:\;}(({Smoke} \land {Heat}) {\:\;{\Rightarrow}\:\;}{Fire}) $

7. ${Big} \lor {Dumb} \lor ({Big} {\:\;{\Rightarrow}\:\;}{Dumb})$

Decide whether each of the following
sentences is valid, unsatisfiable, or neither. Verify your decisions
using truth tables or the equivalence rules of
Table logical-equivalence-table (page logical-equivalence-table).

1. ${Smoke} {\:\;{\Rightarrow}\:\;}{Smoke}$

2. ${Smoke} {\:\;{\Rightarrow}\:\;}{Fire}$

3. $({Smoke} {\:\;{\Rightarrow}\:\;}{Fire}) {\:\;{\Rightarrow}\:\;}(\lnot {Smoke} {\:\;{\Rightarrow}\:\;}\lnot {Fire})$

4. ${Smoke} \lor {Fire} \lor \lnot {Fire}$

5. $(({Smoke} \land {Heat}) {\:\;{\Rightarrow}\:\;}{Fire})
{\;\;{\Leftrightarrow}\;\;}(({Smoke} {\:\;{\Rightarrow}\:\;}{Fire}) \lor ({Heat} {\:\;{\Rightarrow}\:\;}{Fire}))$

6. ${Big} \lor {Dumb} \lor ({Big} {\:\;{\Rightarrow}\:\;}{Dumb})$

7. $({Big} \land {Dumb}) \lor \lnot {Dumb}$

Any propositional logic sentence is logically equivalent to the assertion that each possible world in which it would be false is not the case. From this observation, prove that any sentence can be written in CNF.

Use resolution to prove the sentence $\lnot A \land \lnot B$ from the clauses in Exercise convert-clausal-exercise.

This exercise looks into the relationship between
clauses and implication sentences.

1. Show that the clause $(\lnot P_1 \lor \cdots \lor \lnot P_m \lor Q)$
is logically equivalent to the implication sentence
$(P_1 \land \cdots \land P_m) {\;{\Rightarrow}\;}Q$.

2. Show that every clause (regardless of the number of
positive literals) can be written in the form
$(P_1 \land \cdots \land P_m) {\;{\Rightarrow}\;}(Q_1 \lor \cdots \lor Q_n)$,
where the $P$s and $Q$s are proposition symbols. A knowledge base
consisting of such sentences is in implicative normal form or **Kowalski
form** Kowalski:1979.

3. Write down the full resolution rule for sentences in implicative
normal form.

According to some political pundits, a person who is radical ($R$) is
electable ($E$) if he/she is conservative ($C$), but otherwise is not
electable.

1. Which of the following are correct representations of this
assertion?

1. $(R\land E)\iff C$

2. $R{\:\;{\Rightarrow}\:\;}(E\iff C)$

3. $R{\:\;{\Rightarrow}\:\;}((C{\:\;{\Rightarrow}\:\;}E) \lor \lnot E)$

2. Which of the sentences in (a) can be expressed in Horn form?

This question considers representing satisfiability (SAT) problems as
CSPs.

1. Draw the constraint graph corresponding to the SAT problem
$$(\lnot X_1 \lor X_2) \land (\lnot X_2 \lor X_3) \land \ldots \land (\lnot X_{n-1} \lor X_n)$$
for the particular case $n5$.

2. How many solutions are there for this general SAT problem as a
function of $n$?

3. Suppose we apply {Backtracking-Search} (page backtracking-search-algorithm) to find *all*
solutions to a SAT CSP of the type given in (a). (To find
*all* solutions to a CSP, we simply modify the basic
algorithm so it continues searching after each solution is found.)
Assume that variables are ordered $X_1,\ldots,X_n$ and ${false}$
is ordered before ${true}$. How much time will the algorithm take
to terminate? (Write an $O(\cdot)$ expression as a function of $n$.)

4. We know that SAT problems in Horn form can be solved in linear time
by forward chaining (unit propagation). We also know that every
tree-structured binary CSP with discrete, finite domains can be
solved in time linear in the number of variables
(Section csp-structure-section). Are these two
facts connected? Discuss.

This question considers representing satisfiability (SAT) problems as
CSPs.

1. Draw the constraint graph corresponding to the SAT problem
$$(\lnot X_1 \lor X_2) \land (\lnot X_2 \lor X_3) \land \ldots \land (\lnot X_{n-1} \lor X_n)$$
for the particular case $n4$.

2. How many solutions are there for this general SAT problem as a
function of $n$?

3. Suppose we apply {Backtracking-Search} (page backtracking-search-algorithm) to find *all*
solutions to a SAT CSP of the type given in (a). (To find
*all* solutions to a CSP, we simply modify the basic
algorithm so it continues searching after each solution is found.)
Assume that variables are ordered $X_1,\ldots,X_n$ and ${false}$
is ordered before ${true}$. How much time will the algorithm take
to terminate? (Write an $O(\cdot)$ expression as a function of $n$.)

4. We know that SAT problems in Horn form can be solved in linear time
by forward chaining (unit propagation). We also know that every
tree-structured binary CSP with discrete, finite domains can be
solved in time linear in the number of variables
(Section csp-structure-section). Are these two
facts connected? Discuss.

Explain why every nonempty propositional clause, by itself, is satisfiable. Prove rigorously that every set of five 3-SAT clauses is satisfiable, provided that each clause mentions exactly three distinct variables. What is the smallest set of such clauses that is unsatisfiable? Construct such a set.

A propositional *2-CNF* expression is a conjunction of
clauses, each containing *exactly 2* literals, e.g.,
$$(A\lor B) \land (\lnot A \lor C) \land (\lnot B \lor D) \land (\lnot
C \lor G) \land (\lnot D \lor G)\ .$$

1. Prove using resolution that the above sentence entails $G$.

2. Two clauses are *semantically distinct* if they are not
logically equivalent. How many semantically distinct 2-CNF clauses
can be constructed from $n$ proposition symbols?

3. Using your answer to (b), prove that propositional resolution always
terminates in time polynomial in $n$ given a 2-CNF sentence
containing no more than $n$ distinct symbols.

4. Explain why your argument in (c) does not apply to 3-CNF.

Prove each of the following assertions:

1. Every pair of propositional clauses either has no resolvents, or all
their resolvents are logically equivalent.

2. There is no clause that, when resolved with itself, yields
(after factoring) the clause $(\lnot P \lor \lnot Q)$.

3. If a propositional clause $C$ can be resolved with a copy of itself,
it must be logically equivalent to $ True $.

Consider the following sentence:

$$[ ({Food} {\:\;{\Rightarrow}\:\;}{Party}) \lor ({Drinks} {\:\;{\Rightarrow}\:\;}{Party}) ] {\:\;{\Rightarrow}\:\;}[ ( {Food} \land {Drinks} ) {\:\;{\Rightarrow}\:\;}{Party}]\ .$$

1. Determine, using enumeration, whether this sentence is valid,
satisfiable (but not valid), or unsatisfiable.

2. Convert the left-hand and right-hand sides of the main implication
into CNF, showing each step, and explain how the results confirm
your answer to (a).

3. Prove your answer to (a) using resolution.

A sentence is in disjunctive normal form(DNF) if it is the disjunction of
conjunctions of literals. For example, the sentence
$(A \land B \land \lnot C) \lor (\lnot A \land C) \lor (B \land \lnot C)$
is in DNF.

1. Any propositional logic sentence is logically equivalent to the
assertion that some possible world in which it would be true is in
fact the case. From this observation, prove that any sentence can be
written in DNF.

2. Construct an algorithm that converts any sentence in propositional
logic into DNF. (*Hint*: The algorithm is similar to
the algorithm for conversion to CNF iven in
Sectio pl-resolution-section.)

3. Construct a simple algorithm that takes as input a sentence in DNF
and returns a satisfying assignment if one exists, or reports that
no satisfying assignment exists.

4. Apply the algorithms in (b) and (c) to the following set of
sentences:

$A {\Rightarrow} B$

$B {\Rightarrow} C$

$C {\Rightarrow} A$

5. Since the algorithm in (b) is very similar to the algorithm for
conversion to CNF, and since the algorithm in (c) is much simpler
than any algorithm for solving a set of sentences in CNF, why is
this technique not used in automated reasoning?

Convert the following set of sentences to
clausal form.

1. S1: $A {\;\;{\Leftrightarrow}\;\;}(B \lor E)$.

2. S2: $E {\:\;{\Rightarrow}\:\;}D$.

3. S3: $C \land F {\:\;{\Rightarrow}\:\;}\lnot B$.

4. S4: $E {\:\;{\Rightarrow}\:\;}B$.

5. S5: $B {\:\;{\Rightarrow}\:\;}F$.

6. S6: $B {\:\;{\Rightarrow}\:\;}C$

Give a trace of the execution of DPLL on the conjunction of these
clauses.

Convert the following set of sentences to
clausal form.

1. S1: $A {\;\;{\Leftrightarrow}\;\;}(B \lor E)$.

2. S2: $E {\:\;{\Rightarrow}\:\;}D$.

3. S3: $C \land F {\:\;{\Rightarrow}\:\;}\lnot B$.

4. S4: $E {\:\;{\Rightarrow}\:\;}B$.

5. S5: $B {\:\;{\Rightarrow}\:\;}F$.

6. S6: $B {\:\;{\Rightarrow}\:\;}C$

Give a trace of the execution of DPLL on the conjunction of these
clauses.

Is a randomly generated 4-CNF sentence with $n$ symbols and $m$ clauses more or less likely to be solvable than a randomly generated 3-CNF sentence with $n$ symbols and $m$ clauses? Explain.

Minesweeper, the well-known computer game, is
closely related to the wumpus world. A minesweeper world is
a rectangular grid of $N$ squares with $M$ invisible mines scattered
among them. Any square may be probed by the agent; instant death follows
if a mine is probed. Minesweeper indicates the presence of mines by
revealing, in each probed square, the *number* of mines
that are directly or diagonally adjacent. The goal is to probe every
unmined square.
1. Let $X_{i,j}$ be true iff square $[i,j]$ contains a mine. Write down
the assertion that exactly two mines are adjacent to \[1,1\] as a
sentence involving some logical combination of
$X_{i,j}$ propositions.
2. Generalize your assertion from (a) by explaining how to construct a
CNF sentence asserting that $k$ of $n$ neighbors contain mines.
3. Explain precisely how an agent can use {DPLL} to prove that a given square
does (or does not) contain a mine, ignoring the global constraint
that there are exactly $M$ mines in all.
4. Suppose that the global constraint is constructed from your method
from part (b). How does the number of clauses depend on $M$ and $N$?
Suggest a way to modify {DPLL} so that the global constraint does not need
to be represented explicitly.
5. Are any conclusions derived by the method in part (c) invalidated
when the global constraint is taken into account?
6. Give examples of configurations of probe values that induce
*long-range dependencies* such that the contents of a
given unprobed square would give information about the contents of a
far-distant square. (*Hint*: consider an
$N\times 1$ board.)

How long does it take to prove
${KB}{\models}\alpha$ using {DPLL} when $\alpha$ is a literal *already
contained in* ${KB}$? Explain.

Trace the behavior of {DPLL} on the knowledge base in Figure pl-horn-example-figure when trying to prove $Q$, and compare this behavior with that of the forward-chaining algorithm.

Write a successor-state axiom for the ${Locked}$ predicate, which applies to doors, assuming the only actions available are ${Lock}$ and ${Unlock}$.

Discuss what is meant by *optimal* behavior in the wumpus
world. Show that the {Hybrid-Wumpus-Agent} is not optimal, and suggest ways to improve it.

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

Section successor-state-section provides some of the successor-state axioms required for the wumpus world. Write down axioms for all remaining fluent symbols.

Modify the {Hybrid-Wumpus-Agent} to use the 1-CNF logical state estimation method described on page 1cnf-belief-state-page. We noted on that page that such an agent will not be able to acquire, maintain, and use more complex beliefs such as the disjunction $P_{3,1}\lor P_{2,2}$. Suggest a method for overcoming this problem by defining additional proposition symbols, and try it out in the wumpus world. Does it improve the performance of the agent?