Ve492: Introduction to Artificial Intelligence
Knowledge-based Agent and Propositional Logic
UM-SJTU Joint Institute Slides adapted from AIMA, UM, CMU
Copyright By PowCoder代写 加微信 powcoder
Learning Objectives
❖ What is knowledge-based agent?
❖ What is a logical agent?
❖ What is propositional logic?
❖ How to perform inference in propositional logic?
❖ Knowledge-based Agents
❖ Propositional Language
❖ Inference Algorithms
Knowledge-based Agent
Knowle?dge Base Inference
Environment
Problem Type
❖ Environment Type:
❖ Partially-observable
❖ Single agent
❖ Deterministic
❖ Discrete
❖ Sequential (AIMA)
❖ Known model
❖ Planning agent instead of reflex agent
❖ Can derive new facts from what it currently knows
Performance
❖ pick up gold = +1000,
❖ get eaten or fall in pit = -100
❖ step = -1
❖ shoot = -10
Environment
❖ move forward,
❖ turn left or right,
❖ pick up,
❖ Stench, ❖ Breeze, ❖ Glitter, ❖ Bump, ❖ Scream
Wumpus World
http://thiagodnf.github.io/wumpus-world-simulator/
High-Level Implementation
function KB-AGENT(percept) returns an action persistent: KB, a knowledge base
t, an integer, initially 0 TELL(KB, PROCESS-PERCEPT(percept, t))
action ← ASK(KB, PROCESS-QUERY(t)) TELL(KB, PROCESS-RESULT(action, t)) t←t+1
return action
So what do we TELL our knowledge base (KB)?
❖ Facts (sentences)
❖ The grass is green
❖ The sky is blue ❖ Rules (sentences)
❖ Eating too much candy makes you sick
❖ When you’re sick you don’t go to school ❖ Percepts and Actions (sentences)
❖ Pat ate too much candy today
What happens when we ASK the agent?
❖ Inference – new sentences created from old ❖ Pat is not going to school today
What language to use?
Formal Language
❖ Syntax: What sentences are allowed?
❖ Semantics:
❖ What are the possible worlds?
❖ Which sentences are true in which worlds? (i.e., definition of truth)
❖ Model theory: how do we define whether a statement is true or not? ❖ Truth and entailment
❖ Proof theory: what conclusion can we draw given a state of partial knowledge? ❖ Soundness and completeness
❖ Knowledge base = set of sentences in a formal language
❖ Declarative approach to building an agent (or other system):
❖ Tell it what it needs to know (or have it Learn the knowledge)
❖ Then it can Ask itself what to do—answers should follow from the KB
❖ Agents can be viewed at the knowledge level
i.e., what they know, regardless of how implemented
❖ A single inference algorithm can answer any answerable question
❖ Cf. a search algorithm answers only “how to get from A to B” questions
Logic Language
❖ Propositional logic
❖ Syntax:PÚ(¬QÙR); XÛ(RÞS)
❖ Possible model: {P=true, Q=true, R=false, S=true, X=true} or 11011
❖ Possible world: interpretations of symbols
❖ Semantics:aÙbistrueinaworldiffaistrueandbistrue(etc.)
❖ First-order logic
❖ Syntax: “x $y P(x,y) Ù ¬Q(Joe,f(x)) Þ f(x)=f(y)
❖ Possible model: Objects o1, o2, o3; P holds for
❖ Possible world: interpretations of objects, predicates, and functions.
❖ Semantics: f(s) is true in a world if s=oj and f holds for oj; etc.
Spectrum of Representations
Search, game-playing MDP, RL
CSPs, planning, propositional logic, Bayes nets, neural nets, RL with function approx.
First-order logic, databases, probabilistic programs
Propositional Logic
Propositional Logic
❖ Variable that can be true or false
❖ Written in capital letters, e.g. A, B, P1,2
❖ Often include True and False
❖ Operators:
❖ A Ù B: A and B (conjunction)
❖ A Ú B: A or B (disjunction) Note: this is not an “exclusive or”
❖ A Þ B: A implies B (implication). If A then B
❖ A Û B: A if and only if B (biconditional)
❖ Sentences
Syntax of Propositional Logic
❖ Given: a set of proposition symbols {X1, X2, …, Xn}
Sentence → AtomicSentence | ComplexSentence AtomicSentence → True | False | Symbol Symbol→X1 |X2 |…|Xn
ComplexSentence → ¬Sentence
| (Sentence Ù Sentence)
| (Sentence Ú Sentence) | (Sentence Þ Sentence) | (Sentence Û Sentence)
Example: Wumpus World
Logical Reasoning
❖ Bij = breeze felt
❖ Sij = stench smelt
❖ Pij = pit here
❖ Wij = Wumpus here
❖ Gij = gold
http://thiagodnf.github.io/wumpus-world-simulator/
Wumpus World: Tell KB
❖ There is no pit in [1, 1]: ❖ R1: ¬𝑃!,!
❖ A square is breezy iff there is a pit in a neighboring square: ❖ R2:𝐵!,!⇔(𝑃!,#∨𝑃#,!)
❖ R3: 𝐵#,! ⇔ (𝑃!,! ∨ 𝑃#,# ∨ 𝑃$,!) ❖…
❖ The first two percepts:
❖ R4: ¬𝐵!,!
❖ R5: 𝐵!,#
Truth from Semantics
❖ A model specifies the truth value of every proposition symbol (e.g., 𝑃, ¬𝑃, True, False)
❖ The truth value of complex sentences is defined in terms of the truth values of its elements:
❖ ¬𝑃,𝑃∧𝑄,𝑃∨𝑄,𝑃⇒𝑄,𝑃⇔𝑄
Truth Tables
𝛂 ∨ 𝛃 is inclusive or, not exclusive
FFFF FTFT TFTF TTTT
Truth Tables
𝛂⇒𝛃 isequivalentto ¬𝛂∨𝛃
FFT FTT TFF TTF
Truth Tables
𝛂 ⇔ 𝛃 is equivalent to (𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)
𝛂 𝛃 𝛂⇒𝛃𝛃⇒𝛂
FF TT FT TF TF FT TT TT
(𝛂⇒𝛃) ∧ (𝛃⇒𝛂)
Semantics of Propositional Logic
Using a given model, check if sentence is true
In other words, does the model satisfy the sentence?
Logical Consequences
❖ Problem: When can we conclude b logically follows from a?
❖ Entailment: determines relation between sentences based on
semantics (from outside)
❖ Inference: generates new sentence from current KB (from inside)
❖ Two closely related, but very different, concepts
❖ How are they related?
❖ How can we perform entailment and inference?
Entailment
Entailment: a ⊨ b (“a entails b” or “b follows from a”) iff in every world where a is true, b is also true
❖ I.e., the a-worlds are a subset of the b-worlds [models(a) Í models(b)] Usually we want to know if KB ⊨ query
❖ models(KB) Í models(query) ❖ In other words
❖ KB removes all impossible models (any model where KB is false)
❖ If query is true in all of these remaining models, we conclude that query
must be true
Entailment and implication are very much related
❖ Howisa⊨banda⟹brelated?
❖ Entailment relates two sentences, while an implication is itself a sentence
Validity and Satisfiability
❖ A sentence is valid if it is true in every model ❖ 𝛼entails𝛽ifandonlyif𝛼⇒𝛽isvalid
❖ A valid sentence is also called tautology
❖ A sentence is satisfiable if it is true in some model
❖ A sentence is unsatisfiable if it is true in no model
❖ Satifiability Problem
❖ For a given sentence 𝛼, find assignments to its symbols that makes 𝛼 true
❖ Instance of CSP
❖ Efficient solver: DPLL (AIMA, Chapter. 7.6.1)
Wumpus World: Model
❖ Possible worlds/models ❖ P1,2 P2,2 P3,1
Wumpus World: KB
❖ Possible worlds/models
❖ P1,2 P2,2 P3,1
❖ Knowledge base
❖ Nothing in [1,1]
❖ Breeze in [2,1]
Wumpus World: Query 1
❖ Possible worlds/models
❖ P1,2 P2,2 P3,1
❖ Knowledge base
❖ Nothing in [1,1]
❖ Breeze in [2,1]
❖ Query 𝛼!:
❖ No pit in [1,2]
Wumpus World: Query 2
❖ Possible worlds/models
❖ P1,2 P2,2 P3,1
❖ Knowledge base
❖ Nothing in [1,1]
❖ Breeze in [2,1]
❖ Query 𝛼”:
❖ No pit in [2,2]
Quiz: Wumpus World
❖ Possible worlds/models
❖ P1,2 P2,2 P3,1
❖ Knowledge base
❖ Nothing in [1,1]
❖ Breeze in [2,1]
❖ Query 𝛼#:
❖ No pit in [3,1]
Sentences as Constraints
Adding a sentence to our knowledge base constrains the number of possible models:
KB: Nothing
Possible Models
false false false false false true false true false false true true
true false false true false true true true false true true true
Sentences as Constraints
Adding a sentence to our knowledge base constrains the number of possible models:
KB: Nothing
KB: [(P ∧ ¬Q) ∨ (Q ∧ ¬P)] ⇒ R
Possible Models
false false false false false true false true false false true true
true false false
true false true true true false true true true
Sentences as Constraints
Adding a sentence to our knowledge base constrains the number of possible models:
false false false
false false true
false true false
false true true
true false false
true false true
true true false
true true true
KB: Nothing
KB: [(P ∧ ¬Q) ∨ (Q ∧ ¬P)] ⇒ R KB: R, [(P ∧ ¬Q) ∨ (Q ∧ ¬P)] ⇒ R
Possible Models
Inference Algorithms
Simple model checking
Efficient Model Checking via Satisfiability Theorem proving
Simple Model Checking
function TT-ENTAILS?(KB, α) returns true or false
return TT-CHECK-ALL(KB, α, symbols(KB) U symbols(α),{})
function TT-CHECK-ALL(KB, α, symbols, model) returns true or false if empty?(symbols) then
if PL-TRUE?(KB, model) then return PL-TRUE?(α, model)
else return true else
P ← first(symbols)
rest ← rest(symbols)
return and (TT-CHECK-ALL(KB, α, rest, model ∪ {P = true})
TT-CHECK-ALL(KB, α, rest, model ∪ {P = false }))
Simple Model Checking, contd.
❖ Same recursion as backtracking
❖ O(2n) time, linear space
❖ We can do much better!
P1=true P2=true
P1=false P2=false
Efficient Model Checking via Satisfiability
❖ Assume we have a hyper-efficient SAT solver (DPLL); how can we use it to test entailment?
❖ Suppose 𝛼 ⊨ 𝛽
❖ Then 𝛼 ⇒ 𝛽 is true in all worlds (Deduction theorem)
❖ Hence ¬(𝛼 ⇒ 𝛽) is false in all worlds
❖ Hence 𝛼 ∧ ¬𝛽 is false in all worlds, i.e., unsatisfiable
❖ So, add the negated conclusion to what you know, test for (un)satisfiability; also known as reductio ad absurdum
❖ Efficient SAT solvers operate on conjunctive normal form
Conjunctive Normal Form (CNF)
❖ Every sentence can be expressed as a conjunction of clauses
❖ A clause is a disjunction of literals
❖ A literal is a symbol or a negated symbol
❖ Conversion to CNF by a sequence of standard transformations:
❖ 𝐵!,!⇔(𝑃!,#∨𝑃#,!)
❖ (𝐵!,! ⇒ (𝑃!,# ∨ 𝑃#,!)) ∧ ((𝑃!,# ∨ 𝑃#,!) ⇒ 𝐵!,!)
❖ (¬𝐵!,! ∨ 𝑃!,# ∨ 𝑃#,!) ∧ (¬(𝑃!,# ∨ 𝑃#,!) ∨ 𝐵!,!)
❖ (¬𝐵!,! ∨ 𝑃!,# ∨ 𝑃#,!) ∧ ((¬𝑃!,# ∧ ¬𝑃#,!) ∨ 𝐵!,!)
❖ (¬𝐵!,! ∨ 𝑃!,# ∨ 𝑃#,!) ∧ (¬𝑃!,# ∨ 𝐵!,!) ∧ (¬𝑃#,! ∨ 𝐵!,!)
Inference via Theorem Proving
❖ KB: set of sentences
❖ Inference rule specifies when:
❖ If certain sentences belong to KB, you can add certain other sentences to KB
❖ Proof (KB ⊢ 𝛼) is a sequence of applications of inference rules starting from KB and ending in 𝛼
❖ Inference is a completely mechanical operation guided by syntax, no reference to possible worlds
Example of Inference Rules
❖ Modus ponens: %⇒’,% ‘
❖ And elimination: %∧’ %
❖ Biconditional elimination: %⇔’ (%⇒’)∧(‘⇒%)
Soundness and Completeness
❖ We want inference to be sound:
❖ IfwecanproveBfromA(A⊢B),thenA⊨B
❖ We would like inference to be complete: ❖ IfA⊨B,thenwecanproveBfromA(A⊢B)
❖ These are properties of the relationship between proof and truth.
PL is Sound and Complete!
❖ Theorem: Sound and complete inference can be achieved in PL with one rule: resolution
❖ More generally, #∨%,¬%∨’
❖ More generally yet, #!∨⋯∨#”∨%,¬%∨’!∨⋯’# #!∨⋯∨#”∨’!∨⋯’#
❖ Only apply on clauses
❖ Not restrictive since any PL sentence can be written CNF
Resolution Algorithm
❖ How to perform inference with resolution?
❖ Show KB ⊨ 𝛼 by showing unsatisfability of (KB ∧ ¬𝛼)
function PL-RESOLUTION(KB, α) returns true or false
inputs: KB, the knowledge base, a sentence in propositional logic
α, the query, a sentence in propositional logic
clauses ← the set of clauses in the CNF representation of KB ∧ ¬α new ← { }
for each pair of clauses Ci, Cj in clauses do
resolvents ← PL-RESOLVE(Ci, Cj)
if resolvents contains the empty clause then return true new ← new ∪ resolvents
if new ⊆ clauses then return false clauses ← clauses ∪ new
Concluding Remarks
❖ Logical Agents
❖ Knowledge-based agents that can reason about the world
❖ Propositional Logic
❖ Syntax vs semantics
❖ Algorithms for drawing logical consequences (entailment and inference)
❖ For more information:
❖ AIMA, Chapter 7 for Logical Agents
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com