Propositional Logic

Download Report

Transcript Propositional Logic

Logical Agents
Chapter 7
Fall 2004
Copyright, 1996 © Dale Carnegie & Associates, Inc.
A knowledge-based agent
Accepting new tasks in explicit goals
Knowing about its world



current state of the world, unseen properties from
percepts, how the world evolves
help deal with partially observable environments
help understand “John threw the brick thru the
window and broke it.” – natural language
understanding
Reasoning about its possible course of actions
Achieving competency quickly by being told
or learning new knowledge
CS 471/598, CBS598 by H. Liu
2
Knowledge Base
A knowledge base (KB) is a set of
representations (sentences) of facts about
the world.
TELL and ASK - two basic operations


to add new knowledge to the KB
to query what is known to the KB
Infer - what should follow after the KB has
been TELLed.
A generic KB agent (Fig 7.1)
CS 471/598, CBS598 by H. Liu
3
Three levels of A KB Agent
Knowledge level (the most abstract)
Logical level (knowledge is of sentences)
Implementation level
Building a knowledge base



A declarative approach - telling a KB agent what it
needs to know
A procedural approach – encoding desired behaviors
directly as program code
A learning approach - making it autonomous
CS 471/598, CBS598 by H. Liu
4
Specifying the environment
The Wumpus world (Fig 7.2) in PEAS




Performance: +1000 for getting the gold, -1000 for being
dead, -1 for each action taken, -10 for using up the arrow
 Goal: bring back gold as quickly as possible
Environment: 4X4, start at (1,1) ...
Actions: Turn, Grab, Shoot, Climb, Die
Sensors: (Stench, Breeze, Glitter, Bump, Scream)
The variants of the Wumpus world



Multiple agents
Mobile wumpus
Multiple wumpuses
CS 471/598, CBS598 by H. Liu
5
Acting & reasoning
Let’s play the wumpus game!
The conclusion: “what a fun game!”
Another conclusion: If the available
information is correct, the conclusion is
guaranteed to be correct.
CS 471/598, CBS598 by H. Liu
6
Representation
Knowledge representation


Syntax - the possible configurations that can
constitute sentences
Semantics - the meaning of the sentences
x > y is a sentence about numbers; the sentence
can be true or false
Entailment: one sentence logically follows
another


 |= , iff  is true,  is also true
Sentences entails sentence w.r.t. aspects follows
aspect (Fig 7.6)
CS 471/598, CBS598 by H. Liu
7
Reasoning
KB entails sentence s if KB is true, s is true

Model checking (Fig 7.5) for two sentences/models
 S1 = “There is no pit in [1,2]”
 S2 = “There is no pit in [2,2]”
An inference procedure


can generate new valid sentences or verify if a
sentence is valid given KB
is sound if it generates only entailed sentences
A proof is the record of operation of a sound
inference procedure
An inference procedure is complete if it can
find a proof for any sentence that is entailed.
CS 471/598, CBS598 by H. Liu
8
Inference
Sound reasoning is called logical inference
or deduction.
A sentence is valid or necessarily true iff it
is true under all possible interpretations in
all possible worlds (a model is a world).
A sentence is satisfiable iff there is some
interpretation in some world for which it is
true.
CS 471/598, CBS598 by H. Liu
9
Logics
A logic consists of the following:


A formal system for describing states of
affairs, consisting of syntax (how to make
sentences) and semantics (to relate
sentences to states of affairs).
The proof theory - a set of rules for
deducing the entailments of a set of
sentences.
Some examples of logics ...
CS 471/598, CBS598 by H. Liu
10
Propositional Logic
In this logic, symbols represent whole
propositions (facts)
e.g., D means “the wumpus is dead”
W1,1 Wumpus is in square (1,1)
S1,1 there is stench in square (1,1).
Propositional logic can be connected using
Boolean connectives to generate sentences
with more complex meanings, but does not
specify how objects are represented.
CS 471/598, CBS598 by H. Liu
11
Other logics
First order logic represents worlds using
objects and predicates on objects with
connectives and quantifiers.
Temporal logic assumes that the world
is ordered by a set of time points or
intervals and includes mechanisms for
reasoning about time.
CS 471/598, CBS598 by H. Liu
12
Other logics (2)
Probability theory allows the
specification of any degree of belief.
Fuzzy logic allows degrees of belief in a
sentence and degrees of truth.
CS 471/598, CBS598 by H. Liu
13
Propositional logic
Syntax

A set of rules to construct sentences:
 and, or, imply, equivalent, not
 literals, atomic or complex sentences
 BNF grammar (Fig 7.7, P205)
Semantics


Specifies how to compute the truth value of
any sentence
Truth table for 5 logical connectives (Fig 7.8)
CS 471/598, CBS598 by H. Liu
14
Inference
Truth tables can be used not only to define
the connectives, but also to test for validity:





If a sentence is true in every row, it is valid.
A truth table for “Premises imply Conclusion”
A simple knowledge base for Wumpus (P208)
KB |= . Let’s check its validity (Fig 7.9)
A truth-table enumeration algorithm (Fig 7.10)
A reasoning system should be able to draw
conclusions that follow from the premises,
regardless of the world to which the
sentences are intended to refer.
CS 471/598, CBS598 by H. Liu
15
Equivalence, validity, and
satisfiability
Logical equivalence  |= and  |= 
Validity: a sentence  is true in all models


Valid sentences are tautologies (P v !P)
Deduction theorem: for any  and ,  |= iff the
sentence ( ) is valid
Satisfiability: a sentence is satisfiable if it is
true in some models

If  is true in a model m, then m satisfies 
Validity and satisfiability: is valid iff ! is
unstatisfiable;  is satisfiable iff ! is not valid
CS 471/598, CBS598 by H. Liu
16
Reasoning Patterns in Prop Logic
 |= iff the sentence ( ^ !) is unstatisfiable

Proof by refutation (or contradiction)
Inference rules


Modus Ponens, AND-elimination, Bicond-elimination
All the logical equivalences in Fig 7.11
A proof is a sequence of applications of
inference rules

An example: neither [1,2] nor [2,1] contains a pit
Monotonicity (consistency): the set of entailed
sentences can only increase as information is
added to KB


For  and , if KB |=  then KB^ |= 
Prop logic and first-order logic are monotonic
CS 471/598, CBS598 by H. Liu
17
Resolution – an inference rule
Unit resolution: l1 v l2 …v lk, m = !li

An example
Full resolution: l1 v l2 …v lk, m1 v…v mn
where li = mj

An example
Soundness of resolution

Considering literal li,
 If it’s true, mj is false, then …
 If it’s false, …
CS 471/598, CBS598 by H. Liu
18
Refutation completeness

Resolution can always be used to either confirm or
refute a sentence
Conjunctive normal form (CNF)



A conjunction of disjunctions of literals
A sentence in k-CNF has exactly k literals per clause
(l1,1 v … v l1,k) ^…^ (ln,1 v …v ln,k)
A simple conversion procedure (turn R2 to CNF,P.
215)
A resolution algorithm (Fig 7.12)

An example (KB= R2^R4, to prove !P1,2, Fig. 7.13)
Completeness of resolution

Ground resolution theorem
CS 471/598, CBS598 by H. Liu
19
Horn cluases
A Horn clause is a disjunction of literals of which
at most one is positive




An example: (!L1,1 v !Breeze V B1,1)
An Horn sentence can be written in the form
P1^P2^…^Pn=>Q, where Pi and Q are nonnegated
atoms
Deciding entailment with Horn clauses can be done in
linear time in size of KB
Inference with Horn clauses can be done thru forward
and backward chaining
 Forward chaining is data driven
 Backward chaining works backwards from the query, goal-
directed reasoning
CS 471/598, CBS598 by H. Liu
20
An Agent for Wumpus
The knowledge base (p208)
Finding pits and wumpus using logical inference
Keeping track of location and orientation
Translating knowledge into action

A1,1^EastA^W2,1=>!Forward
Problems with the propositional agent


too many propositions to handle (“Don’t go forward if…”)
hard to deal with change (time dependent propositions)
CS 471/598, CBS598 by H. Liu
21
Summary
Knowledge is important for intelligent agents
Sentences, knowledge base
Propositional logic and other logics
Inference: sound, complete; valid sentences
Propositional logic impratical for even very
small worlds
Therefore, we need to continue our AI class
...
CS 471/598, CBS598 by H. Liu
22