Transcript Propositional Logic

Propositional Logic
Reading: C. 7.4-7.8, C. 8
Logic: Outline
• Propositional Logic
• Inference in Propositional Logic
• First-order logic
2
Agents that reason logically
• A logic is a:
• Formal language in which knowledge can be
expressed
• A means of carrying out reasoning in the language
• A Knowledge base agent
• Tell: add facts to the KB
• Ask: query the KB
3
Towards General-Purpose AI
• Problem-specific AI (e.g., Roomba)
• Specific data structure
• Need special implementation
• Can be fast
• General –purpose AI (e.g., logic-based)
• Flexible and expressive
• Generic implementation possible
• Can be slow
4
Language Examples
• Programming languages
• Formal, not ambiguous
• Lacks expressivity (e.g., partial information)
• Natural Language
• Very expressive, but ambiguous:
– Flying planes can be dangerous.
– The teacher gave the boys an apple.
• Inference possible, but hard to automate
• Good representation language
• Both formal and can express partial information
• Can accommodate inference
5
Components of a Formal Logic
• Syntax: symbols and rules for combining them
What you can say
• Semantics: Specification of the way symbols (and
sentences) relate to the world
What it means
• Inference Procedures: Rules for deriving new sentences
(and therefore, new semantics) from existing sentences
Reasoning
6
7
8
9
10
11
Semantics
• A possible world (also called a model) is an
assignment of truth values to each propositional
symbol
• The semantics of a logic defines the truth of
each sentence with respect to each possible
world
• A model of a sentence is an interpretation in
which the sentence evaluates to True
• E.g., TodayIsTuesday -> ClassAI is true in model
{TodayIsTuesday=True, ClassAI=True}
• We say {TodayIsTuesday=True, ClassAI=True} is a model of
the sentence
12
Exercise: Semantics
What is the meaning of these two
sentences?
• If Shakespeare ate Crunchy-Wunchies for
breakfast, then Sally will go to Harvard
• If Shakespeare ate Cocoa-Puffs for
breakfast, then Sally will go to Columbia
13
Examples
• What are the models of the following
sentences?
• KB1: TodayIsTuesday -> ClassAI
• KB2: TodayIsTuesday -> ClassAI,
TodayIsTuesday
14
15
16
17
Proof by refutation
• A complete inference procedure
• A single inference rule, resolution
• A conjunctive normal form for the logic
18
19
20
21
22
23
24
25
Example: Wumpus World
• Agent in [1,1] has no breeze
• KB = R2 Λ R4 =
(B1,1<->(P1,2 V P2,1)) Λ⌐B1,1
• Goal: show ⌐P1,2
26
Conversion Example
27
28
Resolution of Example
29
Inference Properties
• Inference method A is sound (or truthpreserving) if it only derives entailed sentences
• Inference method A is complete if it can derive
any sentence that is entailed
• A proof is a record of the progress of a sound
inference algorithm.
30
31
32
Other Types of Inference
• Model Checking
• Forward chaining with modus ponens
• Backward chaining with modus ponens
33
Model Checking
• Enumerate all possible worlds
• Restrict to possible worlds in which the KB
is true
• Check whether the goal is true in those
worlds or not
34
Wumpus Reasoning
• Percepts: {nothing in 1,1; breeze in 2,1}
• Assume agent has moved to [2,1]
• Goal: where are the pits?
• Construct the models of KB based on
rules of world
• Use entailment to determine knowledge
about pits
35
36
Constructing the KB
37
38
Properties of Model Checking
• Sound because it directly implements entailment
• Complete because it works for any KB and
sentence to prove α and always terminates
• Problem: there can be way too many worlds to
check
• O(2n) when KB and α have n variables in total
39
Inference as Search
• State: current set of sentences
• Operator: sound inference rules to derive new
entailed sentences from a set of sentences
• Can be goal directed if there is a particular goal
sentence we have in mind
• Can also try to enumerate every entailed
sentence
40
41
42
43
44
45
46
47
Example
48
Complexity
• N propositions; M rules
• Every possible fact can be establisehd
with at most N linear passes over the
database
• Complexity O(NM)
• Forward chaining with Modus Ponens is
complete for Horn logic
49
50
Example
51