Logical Agents and Constraints in AI
Warm-up:
What is the relationship between number of constraints and number of
possible solutions?
In other words, as the number of the constraints increases,
does the number of possible solutions:
A)
Increase
B)
Decrease
C)
Stay the same
Announcements
Midterm 1 Exam
Tue 10/1, in class
Assignments:
HW3
Due tonight, 10 pm
HW4
Due Tue 9/24, 10 pm
P2: Logic and Planning
Out Thu 9/19
Due Thu 10/3, 10 pm
Recitation and feedback survey on Piazza
Due tomorrow, 10 pm
Sat 10/5, 10 pm
AI: Representation and Problem Solving
Propositional Logic
Instructors: Pat Virtue & Fei Fang
Slide credits: CMU AI, http://ai.berkeley.edu
Logical Agents
Logical agents and environments
?
Knowledge Base
Inference
Wumpus World
Logical Reasoning as a CSP
B
ij
= breeze felt
S
ij
= stench smelt
P
ij
= pit here
W
ij
= wumpus here
G = gold
http://thiagodnf.github.io/wumpus-world-simulator/
A Knowledge-based Agent
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
Logical Agents
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
Logical Agents
Sherlock Agent
Really good knowledge base
Evidence
Understanding of how the world works
(physics, chemistry, sociology)
Really good inference
Skills of deduction
“It’s elementary my dear Watson”
Dr. Strange?
Alan Turing?
Kahn?
Worlds
What are we trying to figure out?
Who, what, when, where, why
Time: past, present, future
Actions, strategy
Partially observable? Ghosts, Walls
Which world are we living in?
Models
How do we represent possible worlds with models and knowledge bases?
How do we then do inference with these representations?
Wumpus World
Possible Models
P
1,2
P
2,2
P
3,1
Wumpus World
Possible Models
P
1,2
P
2,2
P
3,1
Knowledge base
Nothing in [1,1]
Breeze in [2,1]
Wumpus World
Wumpus World
Logic Language
Natural language?
Propositional logic
Syntax:
P
(Q
R)
;
X
1
(Raining
Sunny)
Possible world:
{P
=true,
Q
=true,
R
=false,
S
=true}
or
1101
Semantics:
is true in a world iff is
true and
is true (etc.)
First-order logic
Syntax:
x
y P(x,y)
Q(Joe,f(x))
f(x)=f(y)
Possible world: Objects
o
1
,
o
2
,
o
3
;
P
holds for <
o
1
,
o
2
>;
Q
holds for <
o
3
>;
f
(
o
1
)=
o
1
;
Joe
=
o
3
; etc.
Semantics:
() is true in a world if =
o
j
and holds for
o
j
; etc.
Propositional Logic
Piazza Poll 1
Piazza Poll 2
Piazza Poll 1
Piazza Poll 1
Piazza Poll 2
Propositional Logic
Symbol:
Variable that can be true or false
We’ll try to use capital letters, e.g. A, B, P
1,2
Often include True and False
Operators:
A
: not A
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
Propositional Logic Syntax
Given: a set of proposition symbols {X
1
,
X
2
, …,
X
n
}
(we often add
True
and
False
for convenience)
X
i
is a sentence
If
is a sentence then
is a sentence
If
and
are sentences then
is a sentence
If
and
are sentences then
is a sentence
If
and
are sentences then
is a sentence
If
and
are sentences then
is a sentence
And p.s. there are no other sentences!
𝛂 ∨ 𝛃 is
inclusive or
, not exclusive
Notes on Operators
Truth Tables
𝛂 ∨ 𝛃 is
inclusive or
, not exclusive
𝛂 ∨ 𝛃 is
inclusive or
, not exclusive
𝛂 ⇒ 𝛃 is equivalent to ¬𝛂 ∨ 𝛃
Says who?
Notes on Operators
Truth Tables
𝛂 ⇒ 𝛃 is equivalent to ¬𝛂 ∨ 𝛃
𝛂 ∨ 𝛃 is
inclusive or
, not exclusive
𝛂 ⇒ 𝛃 is equivalent to ¬𝛂 ∨ 𝛃
Says who?
𝛂 ⇔ 𝛃 is equivalent to (𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)
Prove it!
Notes on Operators
Truth Tables
𝛂 ⇔ 𝛃 is equivalent to (𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)
Equivalence: it’s true in all models. Expressed as a logical sentence:
(𝛂 ⇔ 𝛃)
⇔
[(𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)]
Propositional Logical Vocab
Vocab Alert!
Propositional Logic
function
PL-TRUE?
(
,
model
)
returns
true or false
if
is a symbol
then
return
Lookup(
,
model
)
if
Op(
) =
then
return
not
(
PL-TRUE?
(Arg1(
),
model
))
if
Op(
) =
then
return
and
(
PL-TRUE?
(Arg1(
),
model
),
PL-TRUE?
(Arg2(
),
model
))
etc.
(Sometimes called “recursion over syntax”)
Check if sentence is true in given model
In other words, does the model
satisfy
the sentence?
Monty Python Inference
There are ways of telling whether she is a witch
Warm-up:
What is the relationship between number of constraints and number of
possible solutions?
In other words, as the number of the constraints increases,
does the number of possible solutions:
A)
Increase
B)
Decrease
C)
Stay the same
Where is the knowledge in our CSPs?
Piazza Poll 3
What is the relationship between the size of the knowledge base and
number of satisfiable models?
In other words, as the number of the knowledge base rules increases,
does the number of satisfiable models:
A)
Increase
B)
Decrease
C)
Stay the same
Piazza Poll 3
What is the relationship between the size of the knowledge base and
number of satisfiable models?
In other words, as the number of the knowledge base rules increases,
does the number of satisfiable models:
A)
Increase
B)
Decrease
C)
Stay the same
Sentences as Constraints
Adding a sentence to our knowledge base constrains the
number of possible models:
KB: Nothing
Possible
Models
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
Sentences as Constraints
Adding a sentence to our knowledge base constrains the
number of possible models:
KB: Nothing
KB: [(P ∧ ¬Q) ∨ (Q ∧ ¬P)] ⇒ R
KB:
R
, [(P ∧ ¬Q) ∨ (Q ∧ ¬P)] ⇒ R
Possible
Models
Sherlock Entailment
“When you have eliminated the impossible, whatever remains,
however improbable, must be the truth” –
Sherlock Holmes via
Sir Arthur Conan Doyle
(Not quite)
Knowledge base and inference
allow us to remove impossible
models, helping us to see what is
true in all of the remaining
models
Wumpus World
Wumpus World
Wumpus World
Entailment
Entailment
:
|
=
(“
entails
” or “
follows from
”
) iff in every world
where
is true,
is also true
I.e., the
-worlds are a subset of the
-worlds [
models
(
)
models
(
)]
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
is true in all of these remaining models, we conclude that
must be true
Entailment and implication are very much related
However, entailment relates two sentences, while an implication is itself a sentence
(usually derived via inference to show entailment)
Wumpus World
Wumpus World
Wumpus World
Propositional Logic Models
All Possible Models
Model Symbols
Piazza Poll 4
Does the KB entail query C?
All Possible Models
Model Symbols
Knowledge Base
Query
Entailment
:
|
=
“
entails
”
iff in every world
where
is true,
is also true
Piazza Poll 4
Does the KB entail query C?
All Possible Models
Model Symbols
Knowledge Base
Query
Entailment
:
|
=
“
entails
”
iff in every world
where
is true,
is also true
Entailment
How do we implement a logical agent that proves entailment?
Logic language
Propositional logic
First order logic
Knowledge Base
Add known logical rules and facts
Inference algorithms
Theorem proving
Model checking
Simple Model Checking
function
TT-ENTAILS?
(
KB, α
)
returns
true or false
Simple Model Checking, contd.
Same recursion as backtracking
11111…1
0000…0
KB?
α
?
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(2
n
) time, linear space
Can we do better?
11111…1
0000…0
KB?
α
?
Inference: Proofs
A proof is a
demonstration
of entailment between
and
Method 1:
model-checking
For every possible world, if
is true m
ake sure that
is
true too
OK for propositional logic (finitely many worlds); not easy for first-order logic
Method 2:
theorem-proving
Search for a sequence of proof steps (applications of
inference rules
) leading from
to
E.g., from
P
(P
Q)
, infer
Q
by
Modus Ponens
Properties
Sound
algorithm: everything it claims to prove is in fact entailed
Complete
algorithm: every sentence that is entailed can be proved
Simple Theorem Proving: Forward Chaining
Forward chaining applies
Modus Ponens
to generate new facts:
Given
X
1
X
2
… X
n
Y
and
X
1
,
X
2
, …,
X
n
Infer
Y
Forward chaining keeps applying this rule, adding new facts, until
nothing more can be added
Requires KB to contain only
definite clauses
:
(Conjunction of symbols)
symbol
; or
A single symbol (note that
X
is equivalent to
True X
)
Forward Chaining Algorithm
function
PL-FC-ENTAILS?
(
KB
,
q
)
returns
true or false
P
Q
L
M
P
B
L
M
A
P
L
A
B
L
A
B
C
LAUSES
Forward Chaining Algorithm
function
PL-FC-ENTAILS?
(
KB
,
q
)
returns
true or false
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
s
agenda
← a queue of symbols, initially symbols known to be true in
KB
P
Q
L
M
P
B
L
M
A
P
L
A
B
L
A
B
1
2
2
2
2
0
0
C
LAUSES
A
GENDA
C
OUNT
A
false
B
false
L
false
M
false
P
false
Q
false
I
NFERRED
Forward Chaining Example: Proving Q
P
Q
L
M
P
B
L
M
A
P
L
A
B
L
A
B
1
2
2
2
2
0
0
A
false
B
false
L
false
M
false
P
false
Q
false
C
LAUSES
A
GENDA
A B
I
NFERRED
C
OUNT
L
x
xxxx
true
//
1
//
1
x
xxxx
true
//
1
//
0
x
xxxx
true
//
1
//
0
M
x
xxxx
true
//
0
P
x
xxxx
true
//
0
//
0
L
Q
x
x
xxxx
true
Forward Chaining Algorithm
function
PL-FC-ENTAILS?
(
KB
,
q
)
returns
true or false
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
s
agenda
← a queue of symbols, initially symbols known to be true in
KB
while
agenda
is not empty
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
Properties of forward chaining
Theorem: FC is sound and complete for definite-clause KBs
Soundness: follows from soundness of Modus Ponens (easy to check
)
Completeness proof:
1. FC reaches a fixed point where no new atomic sentences are derived
2. Consider the final
inferred
table as a model
m
, assigning true/false to symbols
3. Every clause in the original KB is true in
m
Proof: Suppose a clause
a
1
...
a
k
b
is false in
m
Then
a
1
...
a
k
is true in
m
and
b
is false in
m
Therefore the algorithm has not reached a fixed point!
4. Hence
m
is a model of KB
5. If
KB
|
=
q
,
q
is true in every model of
KB
, including
m
Inference Rules
Notation Alert!
Resolution
Resolution
Knowledge Base
Resolution
Knowledge Base
Resolution
Properties
Forward Chaining is:
Sound
and
complete
for
definite-clause
KBs
Complexity: linear time
Resolution is:
Sound
and
complete
for
any PL
KBs!
Complexity: exponential time
0=7, R=4, W=6, U=2, T=8, F=1; 867 + 867 = 1734
Logical agents in AI rely on constraints to deduce solutions. As the number of constraints increases, the number of possible solutions can either decrease, stay the same, or increase. This relationship is crucial for problem-solving and reasoning in AI systems.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Warm-up: What is the relationship between number of constraints and number of possible solutions? In other words, as the number of the constraints increases, does the number of possible solutions: A) Increase B) Decrease C) Stay the same
Announcements Midterm 1 Exam Tue 10/1, in class Assignments: HW3 Due tonight, 10 pm HW4 Due Tue 9/24, 10 pm P2: Logic and Planning Out Thu 9/19 Due Thu 10/3, 10 pm Recitation and feedback survey on Piazza Due tomorrow, 10 pm Sat 10/5, 10 pm
AI: Representation and Problem Solving Propositional Logic Instructors: Pat Virtue & Fei Fang Slide credits: CMU AI, http://ai.berkeley.edu
Logical Agents Logical agents and environments Agent Environment Sensors Percepts Knowledge Base ? Inference Actuators Actions
Wumpus World Logical Reasoning as a CSP Bij = breeze felt Sij = stench smelt Pij = pit here Wij = wumpus here G = gold http://thiagodnf.github.io/wumpus-world-simulator/
A Knowledge-based Agent functionKB-AGENT(percept) returnsan 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 returnaction
Logical Agents 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
Logical Agents Sherlock Agent Really good knowledge base Evidence Understanding of how the world works (physics, chemistry, sociology) Really good inference Skills of deduction It s elementary my dear Watson Dr. Strange? Alan Turing? Kahn?
Worlds What are we trying to figure out? Who, what, when, where, why Time: past, present, future Actions, strategy Partially observable? Ghosts, Walls Which world are we living in?
Models How do we represent possible worlds with models and knowledge bases? How do we then do inference with these representations?
Wumpus World Possible Models P1,2 P2,2 P3,1
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Nothing in [1,1] Breeze in [2,1]
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Nothing in [1,1] Breeze in [2,1] Query ?1: No pit in [1,2]
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Nothing in [1,1] Breeze in [2,1] Query ?2: No pit in [2,2]
Logic Language Natural language? Propositional logic Syntax: P ( Q R); X1 (Raining Sunny) Possible world: {P=true, Q=true, R=false, S=true} or 1101 Semantics: is true in a world iff is true and is true (etc.) First-order logic Syntax: x y P(x,y) Q(Joe,f(x)) f(x)=f(y) Possible world: Objects o1, o2, o3; P holds for <o1,o2>; Q holds for <o3>; f(o1)=o1; Joe=o3; etc. Semantics: ( ) is true in a world if =oj and holds for oj; etc.
Piazza Poll 1 If we know that ? ? and ? ? are true, what do we know about ? ?? ? ? is guaranteed to be true ? ? is guaranteed to be false i. ii. iii. We don t have enough information to say anything definitive about ? ?
Piazza Poll 2 If we know that ? ? and ? ? are true, what do we know about ?? ? is guaranteed to be true ? is guaranteed to be false i. ii. iii. We don t have enough information to say anything definitive about ?
Piazza Poll 1 If we know that ? ? and ? ? are true, what do we know about ? ?? ? ? ? ? ? ? ? ? ? false false false false true false false false true false true true false true false true false false false true true true true true true false false true true true true false true true true true true true false true false true true true true true true true
Piazza Poll 1 If we know that ? ? and ? ? are true, what do we know about ? ?? ? ? ? ? ? ? ? ? ? false false false false true false false false true false true true false true false true false false false true true true true true true false false true true true true false true true true true true true false true false true true true true true true true
Piazza Poll 2 If we know that ? ? and ? ? are true, what do we know about ?? ? ? ? ? ? ? ? ? ? false false false false true false false false true false true true false true false true false false false true true true true true true false false true true true true false true true true true true true false true false true true true true true true true
Propositional Logic Symbol: Variable that can be true or false We ll try to use capital letters, e.g. A, B, P1,2 Often include True and False Operators: A: not A 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
Propositional Logic Syntax Given: a set of proposition symbols {X1, X2, , Xn} (we often add True and False for convenience) Xi is a sentence If is a sentence then is a sentence If and are sentences then is a sentence If and are sentences then is a sentence If and are sentences then is a sentence If and are sentences then is a sentence And p.s. there are no other sentences!
Notes on Operators ? ? is inclusive or, not exclusive
Truth Tables ? ? is inclusive or, not exclusive ? ? ? ? ? ? ? ? F F F F F F F T T F T F T F T T F F T T T T T T
Notes on Operators ? ? is inclusive or, not exclusive ? ? is equivalent to ? ? Says who?
Truth Tables ? ? is equivalent to ? ? ? ? ? ? ? ? ? F F T T T F T T T T T F F F F T T T F T
Notes on Operators ? ? is inclusive or, not exclusive ? ? is equivalent to ? ? Says who? ? ? is equivalent to (? ?) (? ?) Prove it!
Truth Tables ? ? is equivalent to (? ?) (? ?) ? ? ? ? ? ? (? ?) (? ?) ? ? F F T T T T F T F T F F T F F F T F T T T T T T Equivalence: it s true in all models. Expressed as a logical sentence: (? ?) [(? ?) (? ?)]
Propositional Logical Vocab Literal Atomic sentence: True, False, Symbol, Symbol Vocab Alert! Clause Disjunction of literals: ? ? ? Definite clause Disjunction of literals, exactly one is positive ? ? ? Horn clause Disjunction of literals, at most one is positive All definite clauses are Horn clauses
Propositional Logic Check if sentence is true in given model In other words, does the model satisfy the sentence? function PL-TRUE?( ,model) returns true or false if is a symbol thenreturnLookup( , model) if Op( ) = thenreturn not(PL-TRUE?(Arg1( ),model)) if Op( ) = thenreturn and(PL-TRUE?(Arg1( ),model), PL-TRUE?(Arg2( ),model)) etc. (Sometimes called recursion over syntax )
Warm-up: What is the relationship between number of constraints and number of possible solutions? In other words, as the number of the constraints increases, does the number of possible solutions: A) Increase B) Decrease C) Stay the same Where is the knowledge in our CSPs?
Piazza Poll 3 What is the relationship between the size of the knowledge base and number of satisfiable models? In other words, as the number of the knowledge base rules increases, does the number of satisfiable models: A) Increase B) Decrease C) Stay the same
Piazza Poll 3 What is the relationship between the size of the knowledge base and number of satisfiable models? In other words, as the number of the knowledge base rules increases, does the number of satisfiable models: A) Increase B) Decrease C) Stay the same
Sentences as Constraints Adding a sentence to our knowledge base constrains the number of possible models: P Q R Possible Models false false false KB: Nothing 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: P Q R Possible Models false false false KB: Nothing KB: [(P Q) (Q P)] R 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: P Q R Possible Models false false false KB: Nothing KB: [(P Q) (Q P)] R KB: R, [(P Q) (Q P)] R false false true false true false false true true true false false true false true true true false true true true
Sherlock Entailment When you have eliminated the impossible, whatever remains, however improbable, must be the truth Sherlock Holmes via Sir Arthur Conan Doyle (Not quite) Knowledge base and inference allow us to remove impossible models, helping us to see what is true in all of the remaining models
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Breeze Adjacent Pit Nothing in [1,1] Breeze in [2,1]
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Breeze Adjacent Pit Nothing in [1,1] Breeze in [2,1] Query ?1: No pit in [1,2]
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Breeze Adjacent Pit Nothing in [1,1] Breeze in [2,1] Query ?2: No pit in [2,2]
Entailment Entailment: |= ( entails or follows from ) iff in every world where is true, is also true I.e., the -worlds are a subset of the -worlds [models( ) models( )] 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 is true in all of these remaining models, we conclude that must be true Entailment and implication are very much related However, entailment relates two sentences, while an implication is itself a sentence (usually derived via inference to show entailment)
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Breeze Adjacent Pit Nothing in [1,1] Breeze in [2,1] Entailment: KB |= ? KB entails ? iff in every world where KB is true, ? is also true
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Breeze Adjacent Pit Nothing in [1,1] Breeze in [2,1] Query ?1: Entailment: KB |= ? KB entails ? iff in every world where KB is true, ? is also true No pit in [1,2]
Wumpus World Possible Models P1,2 P2,2 P3,1 Knowledge base Breeze Adjacent Pit Nothing in [1,1] Breeze in [2,1] Query ?2: Entailment: KB |= ? KB entails ? iff in every world where KB is true, ? is also true No pit in [2,2]
Propositional Logic Models All Possible Models A B C 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 1 1 Model Symbols
Entailment: |= entails iff in every world where is true, is also true Piazza Poll 4 Does the KB entail query C? All Possible Models A B C 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 1 1 Model Symbols A 0 1 0 1 0 0 0 1 1 1 1 1 1 0 1 1 B C Knowledge Base A B C 1 1 1 1 0 1 1 1 Query C 0 1 0 1 0 1 0 1
Entailment: |= entails iff in every world where is true, is also true Piazza Poll 4 Does the KB entail query C? All Possible Models A B C 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 1 1 Model Symbols A 0 1 0 1 0 0 0 1 1 1 1 1 1 0 1 1 B C Knowledge Base A B C 1 1 1 1 0 1 1 1 Query C 0 1 0 1 0 1 0 1
Entailment How do we implement a logical agent that proves entailment? Logic language Propositional logic First order logic Knowledge Base Add known logical rules and facts Inference algorithms Theorem proving Model checking
Simple Model Checking functionTT-ENTAILS?(KB, ) returnstrue or false
