9 Logical Agents

9.1 Knowledge-based Agents

Problem-solving agents

The problem-solving agents know things, but only in a very limited, inflexible sense.
- E.g., the 8-puzzle agent cannot deduce that with odd parity cannot be reached from states with even parity
CSP enables some parts of the agent to work domain-independently
- Represent states as assignments of values to variables
- Allow for more efficient algorithms

Motivation

Need to:

Digest heterogenous information
Reason deeply with that information

Language

Natural languages (informal):
- English: “Two divides even numbers”.
- Vietnamese: “Hai là số chẵn”.

Programming languages (formal):

Python:
```
def even(x): 
    return x % 2 == 0
```

C++:

bool even(int x) { 
    return x % 2 == 0; 
}

Logical languages (formal):
- First-order-logic:
  
  \forall x\: \text{Even}(x)\to\text{Divides}(x,2)

Two goals of a logic language

Represent knowledge about the world
Reason with that knowledge

Strength and Problem

Strength: provides expressiveness in a compact way
Problem 1: deterministic, didn’t handle uncertainty (probability addresses this)
Problem 2: rule-based, didn’t allow fine tuning from data (machine learning addresses this)

Knowledge-based agents

Supported by logic
Knowledge-based agents can combine and recombine information to suit myriad purposes.
- Accept new tasks in the form of explicitly described goals
- Achieve competence by learning new knowledge of the environment
- Adapt to changes by updating the relevant knowledge
Knowledge base (KB): A set of sentences or facts in a formal language
- Each sentence represents some assertion about the world.
- Axiom = the sentence that is not derived from other sentences
Inference: Using inference engine to derive (infer) new sentences from old ones
- Add new sentences to the knowledge base and query what is known

A generic knowledge-based agent

Given a percept, the agent adds the percept to its knowledge base, asks the knowledge base for the best action, and tells the knowledge base that it has in fact taken that action.

function kb-agent(percept) returns an action

persistent: KB, a knowledge base
            t, a counter, initially 0, indicating time

    Tell(KB, Make-Percept-Sentence(percept, t))
    action ← Ask(KB, Make-Action-Query(t))
    Tell(KB, Make-Action-Sentence(action, t))
    t ← t + 1
    return action

Building an Agent

Procedural approach
- Encode desired behaviors directly as program code.
Declarative approach to building an agent
- Tell it what it needs to know, then it can Ask itself what to do – answers should follow from the KB
Combined approach \to Partially autonomous
Learning approach \to Fully autonomous
- Provide a knowledge-based agent with mechanisms that allow it to learn for itself

9.2 The Wumpus World

Wumpus World PEAS description

The wumpus world is a cave consisting of rooms connected by passageways

Performance measure
- +1000 for climbing out of the gold
- -1000 for falling into a pit or being eaten by the wumpus
- -1 each action taken
- -10 for using the arrow
- The game ends when agent dies or climbs out of the cave
Environment
- A 4\times4 grid of rooms
- Agent starts in the square [1,1], facing to the right
- The locations of gold and wumpus are random
- Each square can be a pit, with probability 0.2
Actuators: The agent can
- Forward
- Left turn by 90°
- Right turn by 90°
- Shooting kills wumpus if you are facing it (the agent has only one arrow)
- Grabbing picks up gold if in same square
- Releasing drops the gold in same square
Sensors: The agent has five sensors
- In the square containing the wumpus and in the directly (not diagonally) adjacent squares, the agent will perceive a Stench.
- In the squares directly adjacent to a pit, the agent will perceive a Breeze.
- In the square where the gold is, the agent will perceive a Glitter.
- When an agent walks into a wall, it will perceive a Bump.
- When the wumpus is killed, it emits a woeful Scream that can be perceived anywhere in the cave [Stench, Breeze, None, None, None]

Characterize the Wumpus World

Fully Observable
- No – only local perception
Deterministic
- Yes – outcomes exactly specified
Episodic
- No – sequential at the level of actions
Static
- Yes – Wumpus and Pits do not move
Discrete
- Yes
Single-agent
- Yes – Wumpus is essentially a natural feature

Exploring a wumpus world

The first step taken by the agent in the wumpus world. (a) The initial situation, after percept [None, None, None, None, None]. (b) After one move, with percept [None, Breeze, None, None, None].
Two later stages in the progress of the agent. (a) After the third move, with percept [Stench, None, None, None, None]. (b) After the fifth move, with percept [Stench, Breeze, Glitter, None, None].
Breeze in (1,2) and (2,1) \implies no safe actions, assuming pits uniformly distributed, (2,2) has pit with probability 0.86 vs. 0.31
Smell in (1,1) \impliescannot move; can use a strategy of coercion:
- shoot straight ahead
- wumpus was there \implies dead \implies safe
- wumpus wasn’t there \implies safe

9.3 Logic

Logic

Definition

Logics are formal languages for representing information such that conclusions can be drawn

Syntax defines the sentences (statements, formulas) in the language
Semantics define the “meaning” of sentences; i.e., define truth of a sentence in a world

The language of arithmetic

x+2\geq y is a sentence
x^{2}+y> is not a sentence
x+2\geq y is true in a world where x=7,y=1
x+2\geq y is false in a world where x=0,y=6
x+2\geq y is true iff the number x+2 is no less than the number y

Models

Definition

Models are formally structured worlds with respect to which truth can be evaluated. A model m in propositional logic is an assignment of truth values to propositional symbols

3 propositional symbols: A, B, C
2^{3}=8 possible models m_{i}:

Model	A	B	C	Model	A	B	C
m_{1}	true	true	true	m_{5}	false	true	true
m_{2}	true	true	false	m_{6}	false	true	false
m_{3}	true	false	true	m_{7}	false	false	true
m_{4}	true	false	false	m_{8}	false	false	false

Interpretation function/semantic

Definition

Let \alpha be a sentence and m be a model. An interpretation function \mathcal{I}(\alpha,m) returns:

true (1) say that m satisfies \alpha or sometimes m is a model of \alpha
false (0) say that m does not satisfies \alpha

Given a sentence \alpha, \mathcal{M}(\alpha) is the set of all models of \alpha

Entailment

Definition

Let \alpha,\beta be sentences, \alpha entails \beta

\begin{equation} \alpha\models\beta \end{equation}

iff in every model where \alpha is true, \beta is also true or

\begin{equation} \mathcal{M}(\alpha)\subseteq\mathcal{M}(\beta) \end{equation}

Contradiction

Definition

Let \alpha,\beta be sentences, \alpha contradicts \beta iff \mathcal{M}(\alpha)\cap\mathcal{M}(\beta)=\emptyset.

Contradiction vs. entailment

Theorem

Let \alpha,\beta be sentences, \alpha contradicts \beta iff \alpha entails \lnot\beta.

Contingency

Definition

Let \alpha,\beta be sentences, \beta is contingent on \alpha iff

\begin{equation} \emptyset\neq\mathcal{M}(\alpha)\cap\mathcal{M}(\beta)\neq\mathcal{M}(\alpha) \end{equation}

Tell operation

Tell: \alpha=\text{"It is raining"}. Tell[KB, Rain]

Possible responses:

Already knew that: entailment (KB\models\alpha)
Don’t believe that: contradiction (KB\models\lnot\alpha)
Learned something new (update KB): contingent KB\gets KB,\alpha

Ask operation

Ask: \alpha=\text{“Is it raining?”}. Ask[KB, Rain]

Possible responses:

Yes: entailment (KB\models\alpha)
No: contradiction (KB\models\lnot\alpha)
I don’t know: contingent

Wumpus models

Situation after the agent detecting nothing in [1,1], moving right and feel breeze in [2,1]
Consider possible models? (assuming only pits)
- 3 Boolean choices \implies 8 possible models

Knowledge base

The agent building knowledge base KB from wumpus-world rules + observations

Entailment

\alpha_{1} = “[1,2] is safe”, KB\models\alpha_{1}, proved by model checking

Contingency

\alpha_{2} = “[2,2] is safe”, KB\not\models\alpha_{2}

9.4 Propositional Logic

Syntax

Propositional logic (a formal language) is the simplest logic – illustrates basic ideas.

The syntax of propositional logic defines

Constants: True, False
Symbols: stand for propositions A, B, B_{1,1}, P_{2,1}
Logical connectives (operator)

connectives	meaning	example
\lnot	negation (NOT)	\lnot S
\land	conjunction (AND)	S_{1}\land S_{2}
\lor	disjunction (OR)	S_{1}\lor S_{2}
\implies	implication	S_{1}\implies S_{2}
\iff	equivalence, biconditional	S_{1}\iff S_{2}

A BNF (Backus–Naur Form) grammar of sentences in propositional logic, along with operator precedences, from highest to lowest.

\begin{array}{rcl} Sentence & \to & AtomicSentence\mid ComplexSentence\\ AtomicSentence & \to & True\mid False\mid P\mid Q\mid R\mid\dots\\ ComplexSentence & \to & (Sentence)\mid[Sentence]\\ & | & \lnot Sentence\\ & | & Sentence\land Sentence\\ & | & Sentence\lor Sentence\\ & | & Sentence\implies Sentence\\ & | & Sentence\iff Sentence\\ \text{Operator Precedence} & : & \lnot,\land,\lor,\implies,\iff \end{array}

Semantic

The semantics defines the rules for determining the truth of a sentence with respect to a particular model m
- Each model m specifies true/false for each proposition symbol
- Arbitrary sentence can be evaluateed by recursive process PL-True and truth tables

P	Q	\lnot P	P\land Q	P\lor Q	P\implies Q	P\iff Q
false	false	true	false	false	true	true
false	true	true	false	true	true	false
true	false	false	false	true	false	false
true	true	false	true	true	true	true

function PL-True?(alpha, model) returns true/false

    if alpha is a symbol then return Lookup(alpha, model)
    if Op(alpha) = '¬' then return Not(PL-True?(Arg1(alpha), model))
    if Op(alpha) = '∧' then return And(PL-True?(Arg1(alpha), model),
                                     PL-True?(Arg2(alpha), model))
    if Op(alpha) = '∨' then return Or(PL-True?(Arg1(alpha), model),
                                  PL-True?(Arg2(alpha), model))
    if Op(alpha) = '⇒' then return ...
    if Op(alpha) = '⇔' then return ...

Entailment

Problem

Given a set of sentences KB and \alpha. Prove that KB\models\alpha

Method 1: model-checking

Time complexity: O(2^{n}) (if KB and \alpha contain n symbols \to there are 2^{n} models)
Space complexity: O(n) (depth-first)
OK for propositional logic; not easy for first-order logic

Method 2: theorem-proving

Search for a sequence of proof steps (applications of inference rules)

Model checking

function TT-Entails?(KB, alpha) returns true/false

inputs: KB, the knowledge base, a sentence in propositional logic
        alpha, the query, a sentence in propositional logic

    symbols ← a list of the propositional symbols in KB and alpha
    return TT-Check-All(KB, alpha, symbols, ⌀)

function TT-Check-All(KB, alpha, symbols, model) returns true/false

    if Empty?(symbols) then
        if PL-True?(KB, model) then return PL-True?(alpha, model)
        else return true
    else
        P ← First(symbols)
        rest ← Rest(symbols)
        return (TT-Check-All(KB, alpha, rest, model U {P=true})
                and
                TT-Check-All(KB, alpha, rest, model U {P=false}))

Validity

Definition

A sentence is valid if it is true in all models. Valid sentences are also known as tautologies

Theorem (Deduction theorem)

For any sentences \alpha and \beta, \alpha\models\beta if and only if the sentence (\alpha\implies\beta) is valid.

Satisfiability

Definition

A sentence is satisfiable if it is true in, or satisfied by, some model

The SAT problem

The problem of determining the satisfiability of sentences in propositional logic was the first problem proved to be NP-complete

Validity, satisfiability and entailment

Given two sentences \alpha,\beta

\alpha is valid iff \lnot\alpha is unsatisfiable
\alpha is satisfiable iff \lnot\alpha is not valid
\alpha\models\beta iff the sentence (\alpha\land\lnot\beta) is unsatisfiable (refutation or contradiction)

A simple knowledge base in Wumpus world

Symbols for each [x,y] location:

P_{x,y} is true if there is a pit in [x,y].
W_{x,y} is true if there is a wumpus in [x,y], dead or alive.
B_{x,y} is true if the agent perceives a breeze in [x,y].
S_{x,y} is true if the agent perceives a stench in [x,y].

Sentences in Wumpus world

\begin{array}{rcl} s_{1} & : & \lnot P_{1,1}\\ s_{2} & : & B_{1,1}\iff(P_{1,2}\lor P_{2,1})\\ s_{3} & : & B_{2,1}\iff(P_{1,1}\lor P_{2,2}\lor P_{3,1})\\ s_{4} & : & \lnot B_{1,1}\\ s_{5} & : & B_{2,1} \end{array}

Inference in Wumpus world

A truth table constructed for the knowledge base given in the text. KB is true if s_{1} through s_{5} are true, which occurs in just 3 of the 128 rows

B_{1,1}	B_{2,1}	P_{1,1}	P_{1,2}	P_{2,1}	P_{2,2}	P_{3,1}	s_{1}	s_{2}	s_{3}	s_{4}	s_{5}	KB
false	false	false	false	false	false	false	true	true	true	true	false	false
false	false	false	false	false	false	true	true	true	false	true	false	false
\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots
false	true	false	false	false	false	false	true	true	false	true	true	false
false	true	false	false	false	false	true	true	true	true	true	true	true
false	true	false	false	false	true	false	true	true	true	true	true	true
false	true	false	false	false	true	true	true	true	true	true	true	true
false	true	false	false	true	false	false	true	false	false	true	true	false
\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots	\vdots
true	true	true	true	true	true	true	false	true	true	false	true	false

The agent makes some conclusion
- KB\models\lnot P_{1,2} means there is no pit in [1,2]
- KB\not\models\lnot P_{2,2} means there might (or might not) be a pit in [2,2]

9.5 Propositional Inference

Inference framework

Definition

If \ell_{1},\cdots,\ell_{k},m are sentences, then the following is an inference rule: \begin{equation} \frac{\ell_{1},\cdots,\ell_{k}}{m}\quad\frac{(\text{premises})}{(\text{conclusion})} \end{equation}

Note: Rules operate directly on syntax, not on semantics.

Forward inference

Input: set of inference rules Rs.

Repeat until no changes to KB:

Choose set of formulas \ell_{1},\cdots,\ell_{k}\in KB.
If matching rule \frac{\ell_{1},\cdots,\ell_{k}}{m} exists then add m to KB.

Definition

KB derives/proves a sentence \alpha, denoted by \begin{equation} KB\vdash_{Rs}\alpha \end{equation} iff \alpha eventually gets added to KB.

Soundness

Definition

A set of inference rules Rs is sound if whenever KB\vdash_{Rs}\alpha, it is also true that KB\models\alpha or \begin{equation} \{\alpha\mid KB\vdash_{Rs}\alpha\}\subseteq\{\alpha\mid KB\models\alpha\} \end{equation}

Completeness

Definition

A set of inference rules Rs is complete if whenever KB\models\alpha, it is also true that KB\vdash_{Rs}\alpha \begin{equation} \{\alpha\mid KB\models\alpha\}\subseteq\{\alpha\mid KB\vdash_{Rs}\alpha\} \end{equation}

World and representation

if KB is true in the real world, then any sentence \alpha derived from KB by a sound inference procedure is also true in the real world
Sentences are physical configurations of the agent, and reasoning is a process of constructing new physical configurations from old ones. Logical reasoning should ensure that the new configurations represent aspects of the world that actually follow from the aspects that the old configurations represent.

Logical equivalence

Definition

Two sentences \alpha and \beta are logically equivalent if they are true in the same set of models. We denotes as \alpha\equiv\beta

\begin{array}{rcl} (\alpha\land\beta) & \equiv & (\beta\land\alpha)\text{ commutativity of }\land\\ (\alpha\lor\beta) & \equiv & (\beta\lor\alpha)\text{ commutativity of }\lor\\ ((\alpha\land\beta)\land\gamma) & \equiv & (\alpha\land(\beta\land\gamma))\text{ associativity of }\land\\ ((\alpha\lor\beta)\lor\gamma) & \equiv & (\alpha\lor(\beta\lor\gamma))\text{ associativity of }\lor\\ \lnot(\lnot\alpha) & \equiv & \alpha\text{ double-negation elimination}\\ (\alpha\implies\beta) & \equiv & (\lnot\beta\implies\lnot\alpha)\text{ contraposition}\\ (\alpha\implies\beta) & \equiv & (\lnot\alpha\lor\beta)\text{ implication elimination}\\ (\alpha\iff\beta) & \equiv & ((\alpha\implies\beta)\land(\beta\implies\alpha))\text{ biconditional elimination}\\ \lnot(\alpha\land\beta) & \equiv & (\lnot\alpha\lor\lnot\beta)\text{ De Morgan}\\ \lnot(\alpha\lor\beta) & \equiv & (\lnot\alpha\land\lnot\beta)\text{ De Morgan}\\ (\alpha\land(\beta\lor\gamma)) & \equiv & ((\alpha\land\beta)\lor(\alpha\land\gamma))\text{ distributivity of }\land\text{ over }\lor\\ (\alpha\lor(\beta\land\gamma)) & \equiv & ((\alpha\lor\beta)\land(\alpha\lor\gamma))\text{ distributivity of }\lor\text{ over }\land \end{array}

Inference rule approach

Theorem proving: Apply rules of inference directly to the sentences in KB to construct a proof of the desired sentence without consulting models.
- More efficient than model checking when the number of models is large but the length of the proof is short
- Legitimate (sound) generation of new sentences from old
Proof = a sequence of inference rule applications to the desired goal
- Can use inference rules as operators in a standard search algorithm. Typically require translation of sentences into a normal form
Note: Logical systems is monotonicity, which says that the set of entailed sentences can only increase as information is added to the knowledge base. For any sentences \alpha and \beta, if KB\models\alpha then KB\land\beta\models\alpha

Important inference rules

Modus ponens	\dfrac{\alpha\implies\beta,\hspace*{1em}\alpha}{\beta}
Modus tollens	\dfrac{\alpha\implies\beta,\hspace*{1em}\lnot\beta}{\lnot\alpha}
And-introduction	\dfrac{\alpha,\hspace*{1em}\beta}{\alpha\land\beta}
And-elimination	\dfrac{\alpha\land\beta}{\alpha}

Example 1

Problem Given KB=\{P\land Q,P\implies R,Q\land R\implies S\}, prove that KB\models S

Solution

#	Sentence	Explanation
s_{1}	P\land Q	from KB
s_{2}	P\implies R	from KB
s_{3}	Q\land R\implies S	from KB
s_{4}	P	(1) and-elimination
s_{5}	R	(4,2) modus ponens
s_{6}	Q	(1) and-elimination
s_{7}	Q\land R	(5,6) and-introduction
s_{8}	S	(3,7) modus ponens

Example 2

Problem In Wumpus wolrd, given KB=\{s_{1},s_{2},s_{3},s_{4},s_{5}\}, prove that KB\models\lnot P_{1,2}

Solution

#	Sentence	Explanation
s_{1}	\lnot P_{1,1}	from KB
s_{2}	B_{1,1}\iff(P_{1,2}\lor P_{2,1})	from KB
s_{3}	B_{2,1}\iff(P_{1,1}\lor P_{2,2}\lor P_{3,1})	from KB
s_{4}	\lnot B_{1,1}	from KB
s_{5}	B_{2,1}	from KB
s_{6}	(B_{1,1}\implies(P_{1,2}\lor P_{2,1}))\land((P_{1,2}\lor P_{2,1})\implies B_{1,1})	Bi-conditional elimination to s_{2}
s_{7}	(P_{1,2}\lor P_{2,1})\implies B_{1,1}	And-elimination to s_{6}
s_{8}	\lnot B_{1,1}\implies\lnot(P_{1,2}\lor P_{2,1})	Contrapositives to s_{7}
s_{9}	\lnot(P_{1,2}\lor P_{2,1})	Modus ponens to s_{4},s_{8}
s_{10}	\lnot P_{1,2}\land\lnot P_{2,1}	De Morgan’s rule to s_{9}
s_{11}	\lnot P_{1,2}	And-elimination to s_{10}

Proving by search

Any search algorithms can be applied to find a sequence of steps that constitutes a proof:

INITIAL STATE: the initial knowledge base KB.
ACTIONS: the set of actions consists of all the inference rules applied to all the sentences that match the top half of the inference rule.
RESULT: the result of an action is to add the sentence in the bottom half of the inference rule.
GOAL: the goal is a state that contains the sentence we are trying to prove.

Conjunctive Normal Form

Definition

Conjunctive Normal Form (CNF—universal)

\begin{array}{cc} \text{conjunction}\text{ of } & \underbrace{\text{disjunctions of }literals}\\ & clauses \end{array}

A BNF (Backus–Naur Form) grammar for conjunctive normal form

\begin{array}{rcl} CNFSentence & \to & Clause_{1}\land...\land Clause_{n}\\ Clause & \to & Literal_{1}\lor...\lor Literal_{m}\\ Literal & \to & Symbol\mid\lnot Symbol\\ Symbol & \to & P\mid Q\mid R... \end{array}

Conversion to CNF

Given a sentence B_{1,1}\iff(P_{1,2}\lor P_{2,1})

Eliminate \iff, replacing \alpha\iff\beta with (\alpha\implies\beta)\land(\beta\implies\alpha). (B_{1,1}\implies(P_{1,2}\lor P_{2,1}))\land((P_{1,2}\lor P_{2,1})\implies B_{1,1})
Eliminate \implies, replacing \alpha\implies\beta with \lnot\alpha\lor\beta. (\lnot B_{1,1}\lor P_{1,2}\lor P_{2,1})\land(\lnot(P_{1,2}\lor P_{2,1})\lor B_{1,1})
Move \lnot inwards using de Morgan’s rules and double-negation: (\lnot B_{1,1}\lor P_{1,2}\lor P_{2,1})\land((\lnot P_{1,2}\land\lnot P_{2,1})\lor B_{1,1})
Apply distributivity law (\lor over \land) and flatten: (\lnot B_{1,1}\lor P_{1,2}\lor P_{2,1})\land(\lnot P_{1,2}\lor B_{1,1})\land(\lnot P_{2,1}\lor B_{1,1})

Resolution inference rule

Resolution inference rule (for CNF):

\begin{equation} \frac{\ell_{1}\lor\cdots\lor{\color{red}\ell_{i}}\lor\cdots\lor\ell_{k},\qquad m_{1}\lor\cdots\lor{\color{green}m_{j}}\lor\cdots\lor m_{n}}{\ell_{1}\lor\cdots\lor\ell_{i-1}\lor\ell_{i+1}\lor\cdots\lor\ell_{k}\lor m_{1}\lor\cdots\lor m_{j-1}\lor m_{j+1}\lor\cdots\lor m_{n}} \end{equation}

where \ell_{i} and m_{j} are complementary literals

Theorem

Resolution inference rule is sound and complete for CNF KB

The resolution algorithm

Proof by contradiction: To show that KB\models\alpha, prove that KB\land\lnot\alpha is unsatisfiable

function PL-Resolution(KB, alpha) returns true/false

inputs: KB, the knowledge base, a sentence in propositional logic
        alpha, the query, a sentence in propositional logic

    clauses ← the set of clauses in the CNF representation of KB & !alpha
    new ← ⌀
    loop do
        for each pair of clauses C_i, C_j in clauses do
            resolvents ← PL-Resolve(C_i, C_j)
            if resolvents contains the empty clause then return true
            new ← new U resolvents
        if new is subset of clauses then return false
        clauses ← clauses U new

Example 3

KB=\left\{ (B_{1,1}\iff(P_{1,2}\lor P_{2,1}))\land\lnot B_{1,1}\right\} and \alpha=\lnot P_{1,2}
Partial application of PL-Resolution to a simple inference in the wumpus world. \lnot P_{1,2} is shown to follow from the first four clauses in the top row
Note: many resolution steps are pointless.

Horn Form

In many practical situations, the full power of resolution is not needed. Some real-world knowledge bases satisfy certain restrictions (Horn form) on the form of sentences

Definition

Horn Form (restricted)

conjunction of Horn clauses

A BNF (Backus–Naur Form) grammar for Horn form \begin{array}{rcl} HornClauseForm & \to & DefiniteClauseForm\mid Symbol\\ DefiniteClauseForm & \to & (Symbol_{1}\land...\land Symbol_{n})\implies Symbol\\ Symbol & \to & P\mid Q\mid R... \end{array}

Modus ponens inference rule

Modus ponens inference rule (for Horn Form)

\begin{equation} \frac{\alpha_{1},\ldots,\alpha_{n},\alpha_{1}\land\cdots\land\alpha_{n}\implies\beta}{\beta} \end{equation}
Can be used with forward chaining or backward chaining.
These algorithms are very natural and run in linear time

Theorem

Modus ponens inference rule is sound and complete for Horn KB

Forward chaining (FC)

Idea: fire any rule whose premises are satisfied in the KB, add its conclusion to the KB, until query is found
Example: Given the following KB, prove that KB\models Q

P\implies Q

L\land M\implies P

B\land L\implies M

A\land P\implies L

A\land B\implies L

A

B
The corresponding AND–OR graph.

The forward-chaining algorithm

function PL-FC-Entails?(KB, q) returns true/false

inputs: KB, the knowledge base, a set of propositional definite clauses
        q, the query, a proposition symbol

    count ← a table, where count[c] is the number of symbols in c's premise
    inferred ← a table, where inferred[s] is initially false for all symbols
    agenda ← a queue of symbols, initially symbols known to be true in KB

    while agenda ≠ ⌀ do
        p ← Pop(agenda)
        if p = q then return true
        if inferred[p] = false then
            inferred[p] ← true
        for each clause c in KB where p is in c.Premise do
            decrement count[c]
            if count[c] = 0 then add c.Conclusion to agenda
    return false

Proof of completeness

FC derives every atomic sentence that is entailed by KB

FC reaches a fixed point where no new atomic sentences are derived
Consider the final state as a model m, assigning true/false to symbols
Every clause in the original KB is true in m

Proof: Suppose a clause a_{1}\land\ldots\land a_{k}\Rightarrow b is false in m
- Then a_{1}\land\ldots\land a_{k} is true in m and b is false in m
- Therefore the algorithm has not reached a fixed point!
Hence m is a model of KB
If KB\models q, q is true in every model of KB, including m

General idea: construct any model of KB by sound inference, check \alpha

Forward chaining example

Backward chaining (BC)

Idea: work backwards from the query q:

To prove q by BC,
check if q is known already, or
prove by BC all premises of some rule concluding q
Avoid loops: check if new subgoal is already on the goal stack
Avoid repeated work: check if new subgoal
1. has already been proved true, or
2. has already failed

Backward chaining example

Forward vs. backward chaining

FC is data-driven, cf. automatic, unconscious processing,
- e.g., object recognition, routine decisions
- May do lots of work that is irrelevant to the goal
BC is goal-driven, appropriate for problem-solving,
- e.g., Where are my keys? How do I get into a PhD program?
- Complexity of BC can be much less than linear in size of KB

9.6 Propositional Model Checking

Efficient propositional inference

Problem The SAT problem is checking satisfiability of sentence \alpha

Two families of efficient algorithms for general propositional inference based on model checking

Complete backtracking search algorithms
- DPLL algorithm (proposed by Davis, Putnam, Logemann and Loveland)
Incomplete local search algorithms (hill-climbing)
- WalkSAT algorithm

Application of SAT: testing entailment, \alpha\models\beta, can be done by testing unsatisfiability of \alpha\land\lnot\beta.

DPLL

The DPLL algorithm

Determine whether an input propositional logic sentence (in CNF) is satisfiable
A recursive, depth-first enumeration of possible models.
Improvements over truth table enumeration
1. Early termination
2. Pure symbol heuristic
3. Unit clause heuristic
Early termination
- A clause is true if any literal is true.
- A sentence is false if any clause is false.
- Avoid examination of entire subtrees in the search space
- E.g., (B\lor C)\land(B\lor D) is true if B is true, regardless C and D
Pure symbol heuristic
- Pure symbol: always appears with the same sign in all clauses.
- Make a pure symbol literal true \to can never make a clause false
- For example, given a sentence (A\lor\lnot B),(\lnot B\lor\lnot C),(A\lor C) \to the symbols A and B are pure, C is impure.
Unit clause heuristic
- Unit clause: only one literal in the clause \to the only literal in a unit clause must be true \to cause “cascade” of forced assignments (unit propagation)
- For example, given a sentence B,\lnot B\lor\lnot C, if the model contains B=true then C=false

Algorithm

function DPLL-Satisfiable?(s) returns true/false

inputs: s, a sentence in propositional logic.

    clauses ← the set of clauses in the CNF representation of s
    symbols ← a list of the proposition symbols in s
    return DPLL(clauses, symbols, {})

function DPLL(clauses, symbols, model) returns true/false

    if every clause in clauses is true in model then return true
    if some clause in clauses is false in model then return false
    P, value ← Find-Pure-Symbol(symbols, clauses, model)
    if P ≠ ⌀ then
        return DPLL(clauses, symbols-P, model U {P=value})
    P, value ← Find-Unit-Clause(clauses, model)
    if P ≠ ⌀ then
        return DPLL(clauses, symbols-P, model U {P=value})
    P ← First(symbols)
    rest ← Rest(symbols)
    return DPLL(clauses, rest, model U {P=true}) 
        or DPLL(clauses, rest, model U {P=false})

Success of DPLL

1962 – DPLL invented
1992 – 300 propositions
1997 – 600 propositions (satz)
2002 (zChaff) 1,000,000 propositions – encodings of hardware verification problems

WalkSAT

The WalkSAT algorithm

Evaluation function: The min-conflict heuristic of minimizing the number of unsatisfied clauses
Balance between greediness and randomness
When the algorithm returns a model
- The input sentence is indeed satisfiable
When it returns failure
- The sentence is unsatisfiable OR we need to give it more time
WalkSAT cannot always detect unsatisfiability
It is most useful when a solution is expected to exist. For example,
- An agent cannot reliably use WalkSAT to prove that a square is safe in the Wumpus world.
- Instead, it can say, “I thought about it for an hour and couldn’t come up with a possible world in which the square isn’t safe.”

Algorithm

function WalkSAT(clauses, p, max_flips) returns a satisfying model or failure

inputs: clauses, a set of clauses in propositional logic
        p, the probability of choosing to do a random walk move,
        typically around 0.5
        max_flips, number of flips allowed before giving up

    model ← a random assignment of true/false to the symbols in clauses
    for i = 1 to max_flips do
        if model satisfies clauses then return model
        clause ← a randomly selected clause from clauses that is false in model
        with probability p
            flip the value in model of a randomly selected symbol from clause
        else
            flip whichever symbol in clause maximizes the number of satisfied clauses
    return failure

9.7 Propositional Logic Based Agent

Propositional Logic Based Agent

Agent has to act given only local perception
Agent is installed with two kinds of knowledge base
- “Hardcode” knowledge base
  
  IF glitter THEN grab gold
  
  IF wumpus or pit around THEN avoid it
- “Softcode” knowledge base KB \begin{array}{l} \lnot P_{1,1},\lnot W_{1,1}\\ B_{x,y}\iff(P_{x,y+1}\lor P_{x,y-1}\lor P_{x+1,y}\lor P_{x-1,y})\\ S_{x,y}\iff(W_{x,y+1}\lor W_{x,y-1}\lor W_{x+1,y}\lor W_{x-1,y})\\ W_{1,1}\lor W_{1,2}\lor...\lor W_{4,3}\lor W_{4,4}\\ \lnot W_{1,1}\lor\lnot W_{1,2},... \end{array}

For a 4\times4 wumpus world, the KB begin with a total of 155 sentences containing 64 distinct symbols

Algorithm

function PL-Wumpus-Agent(percept) returns an action

inputs: percept, a list, [stench, breeze, glitter]
static: KB, a knowledge base
        x, y, , the agent’s position (initially 1,1)
        orientation, orientation (initially right)
        visited, an array indicating which squares have been visited,
                 initially false
        action, the agent’s most recent action, initially null
        plan, an action sequence, initially empty

    update x, y, orientation, visited based on action
    if stench then Tell(KB, S_{x,y}) else Tell(KB, !S_{x,y})
    if breeze then Tell(KB, B_{x,y}) else Tell(KB, !B_{x,y})
    if glitter then action ← grab
    else if plan ≠ ⌀ then action ← Pop(plan)
    else if for some fringe square [i,j], Ask(KB, (!P_{i,j} & !W_{i,j})) is true or
            for some fringe square [i,j], Ask(KB, (P_{i,j} | W_{i,j})) is false then
        plan ← A*-Graph-Search(Route-Problem([x,y], orientation, [i,j], visited))
        action ← Pop(plan)
    else action ← a randomly chosen move
    return action

9.1 Knowledge-based Agents

Problem-solving agents

Motivation

Language

Two goals of a logic language

Strength and Problem

Knowledge-based agents

A generic knowledge-based agent

Building an Agent

9.2 The Wumpus World

Wumpus World PEAS description

Characterize the Wumpus World

Exploring a wumpus world

9.3 Logic

Logic

Models

Interpretation function/semantic

Entailment

Contradiction

Contradiction vs. entailment

Contingency

Tell operation

Ask operation

Wumpus models

Knowledge base

Entailment

Contingency

9.4 Propositional Logic

Syntax

Semantic

Entailment

Model checking

Validity

Satisfiability

Validity, satisfiability and entailment

A simple knowledge base in Wumpus world

Inference in Wumpus world

9.5 Propositional Inference

Inference framework

Forward inference

Soundness

Completeness

World and representation

Logical equivalence

Inference rule approach

Important inference rules

Example 1

Example 2

Proving by search

Conjunctive Normal Form

Conversion to CNF

Resolution inference rule

The resolution algorithm

Example 3

Horn Form

Modus ponens inference rule

Forward chaining (FC)

The forward-chaining algorithm

Proof of completeness

Forward chaining example

Backward chaining (BC)

Backward chaining example

Forward vs. backward chaining

9.6 Propositional Model Checking

Efficient propositional inference

DPLL

The DPLL algorithm

Algorithm

Success of DPLL

WalkSAT

The WalkSAT algorithm

Algorithm

9.7 Propositional Logic Based Agent

Propositional Logic Based Agent

Algorithm

9.8 References