7-LogicalAgents

Download Report

Transcript 7-LogicalAgents

Logical Agents
•
Knowledge-Based Agents
• Logic
• Propositional Logic
• Summary
Knowledge-Based Agents
• Central component is a knowledge-base
• Knowledge is made of sentences
• Sentences are expressed in a language
• We wish to derive new sentences through
inference.
Knowledge-Based Algorthim
Function KB (percept) returns action
TELL (KB; PERCEPT-SENTENCE(percept,t))
action = ASK(KB,MAKE-ACTION-QUERY(t))
TELL (KB;ACTION-SENTENCE(action,t))
T=t+1
Return action
Declarative vs Procedural
Two approaches to store knowledge:
1. Declarative.
Sentences representing knowledge
2. Procedural.
Encode behavior directly as code.
An Example
Moving on a square to reach a goal
state while avoiding risks.
Logical Agents
•
Knowledge-Based Agents
• Logic
• Propositional Logic
• Summary
Logic
Important terms:
 Syntax .- rules to represent well-formed
sentences
 Semantics.- define the truth of each sentence.
 Model.- Possible world (m is a model of a)
 Entailment:
a |= b
a entails b means:
In every model where a is true, b is also true.
Logic
Sentence a is derived from KB by algorithm i:
KB |=i a
• Algorithm i is called sound (truth preserving) if
it derives only entailed sentences.
• Algorithm i is called complete if it derives all
entailed sentences.
Physical configuration
Sentence
Sentence
entails
Representation
Real World
follows
Real World
Allen Newell
Born in 1927 – died in 1992
1982 “The Knowledge Level”
Rational agents can be described
by the knowledge they contain
With Herbert Simon he developed the
Logic Theorist (first real AI program).
Winner of the Turing Award
Logical Agents
•
Knowledge-Based Agents
• Logic
• Propositional Logic
• Summary
Syntax
• Atomic sentences: propositional symbols
• Complex sentences use logical connectives
• Negation,conjunction,disjunction
• Implication and biconditional.
Syntax
Sentence
Atom
Symbol
Complex S
 Atom | Complex Structure
 True | False | Symbol
 P|Q|R
 - sentence
| ( sentence ^ sentence )
| ( sentence V sentence )
| ( sentence  sentence)
| ( sentence  sentence)
Semantics
How to define the truth value of statements?
• Connectives associate to truth tables.
• The knowledge base of an agent grows by
telling it of new statements:
TELL(KB,S1), … TELL(KB,Sn)
KB = S1 ^ … ^ Sn
Inference
We want to know if KB entails a: KB |= a
Approach 1: Try all models
KB: {b , b  a}
ba
t t
t f
f t
f f
Models consistent with KB
YES
NO
NO
NO
Check All Models
Method is characterized as:
• sound (directly implements entailment)
• complete (it works for any KB and a and
it always terminates.
Problem: With n symbols there are 2n models.
Time complexity is O(2n)
Space complexity is O(n)
Some concepts
• Equivalence:
a = b  a |= b and b |= a
•Validity
A sentence is valid if it is true in all models
Example p V -p
•Satisfiability
A sentence is satisfiable if it is true in some
model
Reasoning Patterns




Modus Ponens
a  b, a
b
And-Elimination
a^b
a
Commutativity of ^ and V
de Morgan’s Laws, etc.
Proofs
• Applying a sequence of rules is called a proof.
• Equivalent to searching for a solution
• Monotonicity: if KB |= a then KB ^ b |= a
{b, b a}
Modus ponens
a
Resolution
Complete and sound inference algorithm
avb
~a v c
bvc
Cannot derive all conclusions but can tell
if they are true or false (refutation completeness).
Applying Resolution
Resolution only works on disjunction of literals.
How can we apply resolution to all clauses?
Solution: convert to conjunctive normal form (CNF)
CNF : (L11 V .. V L1k) ^ … ^ (Ln1 V … V Lnk)
Resolution
How does it work?
To show that KB |= a
We show that (KB ^ ~a) is unsatisfiable.
Every pair that contains complementary literals is
resolved.
Continue until there are no new clauses (KB |= a)
Or we derive the empty clause (a V ~a) (KB |= a)
Example
a v b v ~c
KB
dvc
avbvd
~b
avd
KB |= b
~d
a
~a
Horn Clauses
In practice we restrict our clauses to Horn Clauses.
(base of logic programming)
Horn Clause: disjunction of literals with at most
one of them being positive.
Example: (~a v ~b v c)
(definite clause)
Equivalent to ( a ^ b  c )
Forward Chaining
Begins from known facts in the knowledge base.
If premises of implication are known derive
conclusion.
Continue until query is added or no more
inferences can be made.
a^b^cd
a,b,c
conclude d
Example
Q
PQ
L^MP
B^LM
A^PL
A^BL
A
B
P
M
L
A
B
AND-OR Graph
Backward Chaining
Works backwards from the query q
Find implications that conclude q
If all premises can be proved true then q is true
a^b^cq
How do I prove a? and b? and c?
Logical Agents
•
Knowledge-Based Agents
• Logic
• Propositional Logic
• Summary
Summary
• Rational agents need to work with knowledge bases.
• A language is defined by syntax and semantics
• KB |= a if a is true in all models where KB is true
• Inference techniques can be characterized based
on soundness and completeness.
• Simplest logic is propositional logic
• A strong inference rule is called “resolution”
• When using Horn clauses, reasoning methods
are forward and backward chaining.