Symbolic Representation and Reasoning
Download
Report
Transcript Symbolic Representation and Reasoning
Symbolic
Representation and Reasoning
an Overview
Stuart C. Shapiro
Department of Computer Science and Engineering,
Center for Multisource Information Fusion,
and Center for Cognitive Science
University at Buffalo, The State University of New York
201 Bell Hall, Buffalo, NY 14260-2000
[email protected]
http://www.cse.buffalo.edu/~shapiro/
Introduction
Knowledge Representation
Reasoning
Symbols
Logics
September, 2004
S. C. Shapiro
2
Knowledge Representation
A subarea of Artificial Intelligence
Concerned with understanding, designing, and
implementing ways of representing information in
computers
So that programs can use this information to
derive information that is implied by it,
to converse with people in natural languages,
to plan future activities,
to solve problems in areas that normally require human
expertise.
September, 2004
S. C. Shapiro
3
Reasoning
Deriving information that is implied by the
information already present is a form of
reasoning.
Knowledge representation schemes are
useless without the ability to reason with
them.
So, Knowledge Representation and Reasoning
September, 2004
S. C. Shapiro
4
Knowledge vs. Belief
Knowledge: Justified True Belief
KR systems operate the same whether or not
the information stored is justified or true.
So, Belief Representation and Reasoning
would be better.
But we’ll stick with KR.
September, 2004
S. C. Shapiro
5
What Is a Symbol?
“A symbol token is a pattern that can be
compared to some other symbol token and judged
equal with it or different from it…
Symbols may be formed into symbol structures
by means of a set of relations…
The `objects’ that symbols designate may include
… objects in an external environment of sensible
(readable) stimuli.”
[Newell & Simon, Concise Encyclopedia of CS, 2004]
September, 2004
S. C. Shapiro
6
What Is Logic?
The study of correct reasoning.
Not a particular KR language.
There are many systems of logic.
With slight abuse, we call a system of logic a logic.
KR research may be seen as the search for the
correct logic(s) to use in intelligent systems.
September, 2004
S. C. Shapiro
7
Parts of Specifying a Logic
Syntax
Semantics
Proof Theory
September, 2004
S. C. Shapiro
8
Syntax
The specification of a set of atomic symbols, and
the grammatical rules for combining them into
well-formed expressions (symbol-structures).
September, 2004
S. C. Shapiro
9
Syntactic Expressions
Atomic symbols
Individual constants: Tom, Betty, white
Variables: x, y, z
Function symbols: motherOf
Predicate symbols: Person, Elephant, Color
Propositions: P, Q, BdT
Terms
Individual constants: Tom, Betty, white
Variables : x, y, z
Functional terms: motherOf(Fred)
Well-formed formulas (wffs)
Propositions (Proposition symbols) : P, Q, BdT
Atomic formulas: Color(x, white), Duck(motherOf(Fred))
Non-atomic formulas: TdB Td Bp
September, 2004
S. C. Shapiro
10
Semantics
The specification of the meaning (designation) of
the atomic symbols, and the rules for determining
the meanings of the well-formed expressions from
the meanings of their parts.
September, 2004
S. C. Shapiro
11
Semantic Values
Terms could denote
Objects
Categories of objects
Properties…
Wffs could denote
Propositions
Truth values
September, 2004
S. C. Shapiro
12
Truth Values
Could be 2, 3, 4, …, ∞ different truth
values.
Some truth values are “distinguished”
Needn’t have anything to do with truth in
the real world.
By default, we’ll assume 2 truth values.
Call distinguished one True (T)
Call other False (F)
September, 2004
S. C. Shapiro
13
Proof Theory
The specification of a set of rules, which, given an
initial collection of well-formed expressions,
specify what other well-formed expressions can
be added to the collection.
September, 2004
S. C. Shapiro
14
Proof / Knowledge Base
The collection could be
A proof
A knowledge base
The initial collection could be
Axioms
Hypotheses
Assumptions
Domain facts & rules
The added expressions could be
Theorems
Derived facts & rules
September, 2004
S. C. Shapiro
15
Example
Logic: Standard Propositional Logic
Domain: CarPool World
Atomic Proposition Symbols:
BdT, TdB, Bd, Td, Bp, Tp
Unary wff-forming connective:
Binary wff-forming connectives: , , ,
September, 2004
S. C. Shapiro
16
Intended Interpretation
(Intensional Semantics)
BdT: Betty drives Tom
TdB: Tom drives Betty
Bd: Betty is the driver
Td: Tom is the driver
Bp: Betty is the passenger
Tp: Tom is the passenger
September, 2004
S. C. Shapiro
17
Extensional (Denotational)
Semantics
BdT
TdB
Bd
T
T
T
T
T
T
T
F
T
F
T
F
F
F
F
Td
Bp
Tp
T
T
T
T
F
F
F
F
F
F
T
T
T
T
F
F
F
F
F
F
T
F
T
F
T
F
T
F
T
F
Bd Tp
Td Td
Td Td
5 of 26 = 64 possible situations
September, 2004
S. C. Shapiro
18
Properties of Wffs
Satisfiable
T in some situation
BdT
T
T
T
F
F
TdB
T
T
F
T
F
Bd
T
T
T
F
F
Td
T
F
F
T
F
Bp
T
F
F
T
F
Tp
T
F
T
F
F
Bd Tp
T
F
T
F
F
Td Td
T
T
T
T
T
Td Td
F
F
F
F
F
September, 2004
S. C. Shapiro
19
Properties of Wffs
Contingent
T in some, F in some
BdT
T
T
T
F
F
TdB
T
T
F
T
F
Bd
T
T
T
F
F
Td
T
F
F
T
F
Bp
T
F
F
T
F
Tp
T
F
T
F
F
Bd Tp
T
F
T
F
F
Td Td
T
T
T
T
T
Td Td
F
F
F
F
F
September, 2004
S. C. Shapiro
20
Properties of Wffs
Valid
T in all situations
BdT
T
T
T
F
F
TdB
T
T
F
T
F
Bd
T
T
T
F
F
Td
T
F
F
T
F
Bp
T
F
F
T
F
Tp
T
F
T
F
F
Bd Tp
T
F
T
F
F
Td Td
T
T
T
T
T
Td Td
F
F
F
F
F
September, 2004
S. C. Shapiro
21
Properties of Wffs
Contradictory
T in no situation
BdT
T
T
T
F
F
TdB
T
T
F
T
F
Bd
T
T
T
F
F
Td
T
F
F
T
F
Bp
T
F
F
T
F
Tp
T
F
T
F
F
Bd Tp
T
F
T
F
F
Td Td
T
T
T
T
T
Td Td
F
F
F
F
F
September, 2004
S. C. Shapiro
22
Logical Implication
P1, …, Pn logically imply Q
P1, …, Pn |= Q
In every situation that P1, …, Pn are True,
so is Q.
September, 2004
S. C. Shapiro
23
Example: CarPool World KB
Let KBCPW =
Bd Bp
Td Tp
BdT Bd Tp
TdB Td Bp
TdB BdT
September, 2004
S. C. Shapiro
24
Extensional (Denotational)
Semantics
BdT
TdB
Bd
T
F
T
F
T
F
Td
Bp
Tp
F
F
T
T
T
F
Only 2 of the 64 situations where KBCPW are T
So, e.g.,
KBCPW, BdT |= Bd Bp
This is how a KB constrains a model to the domain we want.
September, 2004
S. C. Shapiro
25
Proof Theory
Some Rules of Inference
PQ
P
Q
Modus Ponens or Elimination
Q
Elimination
PQ
P
P
Q
PQ
Elimination
September, 2004
PQ
P
Introduction
S. C. Shapiro
26
Derivation from Assumptions
Q is derivable from P1, …, Pn
P1, …, Pn |- Q
Starting from the collection P1, …, Pn,
one can repeatedly apply rules of inference,
and eventually get Q.
September, 2004
S. C. Shapiro
27
Example: CarPool World Proof
BdT Bd Tp
BdT
Bd Bp
Bd Tp
Bd
Bp
Bd Bp
So, KBCPW, BdT |- Bd Bp
September, 2004
S. C. Shapiro
28
Theoremhood
If Q is derivable from no assumptions,
|- Q
We say that Q is provable,
and that Q is a theorem.
September, 2004
S. C. Shapiro
29
Deduction Theorem
P1, …, Pn |= Q iff |= (P1 · · · Pn ) Q
P1, …, Pn |- Q iff |- (P1 · · · Pn ) Q
So theorem-proving is relevant to reasoning.
September, 2004
S. C. Shapiro
30
Properties of Logics
Soundness
If |- P then |= P
(If P is a provable, then P is valid.)
Completeness
If |= P then |- P
(If P is valid, then P is a provable.)
September, 2004
S. C. Shapiro
31
Soundness vs. Completeness
Soundness is the essence of correct reasoning
Completeness is less important because it
doesn’t indicate how long it might take.
September, 2004
S. C. Shapiro
32
Commutativity Diagram
for
Sound and Complete Logics
|= (P1 · · · Pn ) Q
P1, …, Pn |= Q
soundness
soundness
completeness
completeness
|- (P1 · · · Pn ) Q
P1, …, Pn |- Q
So, whenever you want one, you can do another.
September, 2004
S. C. Shapiro
33
Use of Commutativity Diagram
Refutation proof techniques,
such as resolution refutation
or semantic tableaux,
prove that there can be no situation
in which P1, …, and Pn are True
and Q is False.
These are semantic proof techniques.
September, 2004
S. C. Shapiro
34
Decision Procedure
A procedure that is guaranteed
to terminate
and tell whether or not P is provable.
September, 2004
S. C. Shapiro
35
Semidecision Procedure
A procedure that, if P is a theorem
is guaranteed
to terminate
and say so.
Otherwise, it may not terminate.
September, 2004
S. C. Shapiro
36
A Tour of
Some Classes of Logics
Propositional Logics
Elementary Predicate Logics
Full First-Order Logics
September, 2004
S. C. Shapiro
37
Propositional Logics
Smallest Unit: Proposition/Sentence
propositional logics that are
Sound
Complete
Have decision procedures
September, 2004
S. C. Shapiro
38
What You Can Do
with Propositional Logic
• BettyDrivesTom TomDrivesBetty
• BettyDrivesTom NearTomBetty
• TomDrivesBetty NearTomBetty
• NearTomBetty
Can derive conclusions
even though the “facts” aren’t entirely known.
September, 2004
S. C. Shapiro
39
Elementary Predicate Logics
Propositions plus
Predicate (Relation) symbols,
Individual terms, variables, quantifiers
elementary predicate logics that are
Sound
Complete
Have decision procedures
September, 2004
S. C. Shapiro
40
What You Can Say with
Elementary Predicate Logic
• x[Elephant(x) HasA(x, trunk)]
Can state generalities
before all individuals are known.
• x[Elephant(x) Color(x, white)]
Can describe individuals
Even when they are not specifically known.
September, 2004
S. C. Shapiro
41
Full First-Order Logics
Elementary predicate logic plus
Function symbols/ functional terms
full first-order logics that are
Sound
None are
Complete
Have decision procedures
September, 2004
S. C. Shapiro
42
What You Can Say with
Full First-Order Logic
p[HasProp(0, p)
x[HasProp(x, p) HasProp(x+1, p)]
x HasProp(x, p)]
Principle of induction.
September, 2004
S. C. Shapiro
43
Example of Undecidability
• Large KB about ducks, etc.
• x[y (Duck(y) WalksLike(x,y))
y (Duck(y) TalksLike(x,y))
Duck(x)]
• x Duck(motherOf(x)) Duck(x)
• Duck(Fred)?
• If Fred is not a duck, possible ∞ loop.
September, 2004
S. C. Shapiro
44
Unsound Reasoning
Induction
From
Raven(a) Black(a)
Raven(b) Black(b)
Raven(c) Black(c)
Raven(d) Black(d)
…
Raven(n) Black(n)
To
x[Raven(x) Black(x)]
September, 2004
S. C. Shapiro
45
Unsound Reasoning
Abduction
From
x[Person(x) Injured(x) Bandaged(x)]
Person(Tom)
Bandaged(Tom)
To
Injured(Tom)
September, 2004
S. C. Shapiro
46
What’s “First-Order” about
First-Order Logics
Can’t quantify over
Function symbols
Predicate symbols
Propositions
September, 2004
S. C. Shapiro
47
Examples of
SNePS
Reasoning
Using a Logic
Designed for KRR
September, 2004
S. C. Shapiro
48
SNePS, A “Higher-Order” Logic
: all(R)(Transitive(R)
=> (all(x,y,z)(R(x,y) and R(y,z) => R(x,z)))).
: Bigger(elephants, lions).
: Bigger(lions, mice).
: Transitive(Bigger).
: Bigger(elephants, mice)?
Bigger(elephants,mice)
Really a higher-order language for a first-order logic
September, 2004
S. C. Shapiro
49
“Higher-Order” Example 2
: all(source)(Trusted(source)
=> all(p)(Says(source, p) => p)).
: Trusted(Agent007).
: Says(Agent007, Dangerous(Dr_No)).
: Dangerous(Dr_No)?
Dangerous(Dr_No)
September, 2004
S. C. Shapiro
50
Designing New Connectives
: andor(1,1){OnFloor(G2), OnFloor(G1),
OnFloor(1), OnFloor(2)}.
: OnFloor(G1).
: OnFloor(?where)?
~OnFloor(G2)
~OnFloor(1)
~OnFloor(2)
OnFloor(G1)
September, 2004
S. C. Shapiro
51
Belief Change
: andor(1,1){OnFloor(G2), OnFloor(G1), OnFloor(1), OnFloor(2)}.
: {OnFloor(G2), OnFloor(G1)} => {Location(belowGround)}.
: {OnFloor(1), OnFloor(2)} => {Location(aboveGround)}.
: perform believe(OnFloor(G2))
: Location(?where)?
Location(belowGround)
: perform believe(OnFloor(2))
: Location(?where)?
Location(aboveGround)
September, 2004
S. C. Shapiro
52
Summary 1
Symbolic KRR uses logic.
There are many logics.
The question is which to use.
September, 2004
S. C. Shapiro
53
Summary 2
A logic has a
Syntax
Semantics
Proof Theory
Logics may
Be sound
Be complete
Have a decision procedure
September, 2004
S. C. Shapiro
54
Summary 3
Logics provide non-atomic wffs
That can describe situations
Without knowing all specifics
September, 2004
S. C. Shapiro
55
Summary 4
One can design and build
Useful new logics
And reasoning systems using them.
September, 2004
S. C. Shapiro
56