CSE2309/3309 Artificial Intelligence Knowledge Representation I

Dr. Ann Nicholson

School of Computer Science and Software Eng.
Rm 115 Bld 26, annn@csse.monash.edu.au

Overview

• A knowledge-based agent.
• Review of Propositional Logic
• First-Order Predicate Calculus (FOPC): Syntax, Semantics, Inference
• Logic-based agents
• Situation Calculus
• The Frame Problem

Reading:

CSE2309/CSC2030 1999 Lectures 20, 21, 23, 24, 25;

Russell & Norvig, Chapters 6, 7, 9.1-9.6

A knowledge-based agent

Central Components:

• Agent's knowledge base (KB)
  • Set of representations (sentences) of facts about the world.
  • Add new sentences to the KB: TELL.
• Agent's inference mechanism.
  • Query agent what is known: ASK.
  • Answers to ASK should follow from what TELLed.

The Wumpus World (R&N Section 6.2)

The Wumpus World

• Percepts:
  • Wumpus smells; stench noticable in adjacent squares.
  • Breeze noticeable adjacent to pits.
  • Glitter noticeable where gold is.
  • Agent walks into wall, feels bump.
  • Wumpus dies, scream heard everywhere.
• Actions:
  • Go forward, turn right 90, turn left 90.
  • Grab, Shoot (only 1 arrow), Climb, Die.
• Goal: find gold and exit as quickly as possible. Scoring:
  • +1,000 points climbing out of cave with gold;
  • -1 point for each action taken;
  • -10,000 points for dying.

Knowledge Representation Languages

A logic consists of

• Syntax:
  
• Semantics:
  
• Inference procedure (Proof Theory).
  

• Distinguish between facts and representations:
  • Fact: claim about the world, may be true or false.
  • Representations: expressions in some language
• Reasoning is the process of constructing new representations (sentences) from old one.

Basic Properties and Relations

• Truth: depends on the state of the world, the interpretation.
• A sentence is valid if it's true regardless of the world or the semantics.
• A sentence is unsatisfiable if the world is never like what it describes.
• Entailment: whenever one set of sentences is true under an interpretation, so is another sentence.

  
  
  

  • requires the truth of S follow that of P under all interpretations.
• Model: any world which is true under an interpretation is a model of that sentence under that interpretation.
  • Given P and Q, if Q is true in every model in which P is true (relative to semantic interpretation function i) then .
  • If models of KB are all models of , then KB entails .

Inference Procedures

• Inference procedures: mechanical set of rules which can be applied to sentences to determine what they entail.
• Application of rules is inference.
• (, is a set of sentences).
• : is derived from KB by ip.
• Record of derivation = proof.
• Important properties:
  • Soundness: If , then .
  • Completeness: If , then .
• Computing ``entailments".

Logics

• Assuming you recall propositional logic and first-order predicate calculus.
• Ontological commitments:
  • propositional logic: facts that are either true or false.
  • predicate calculus: objects, relations between objects that either hold or don't.
  • temporal logics: set of time intervals or points that order world.
• Epistemological commitments: state of knowledge
  • propositional logic: agent believes sentence to be true or false, or is unable to conclude.
  • predicate calculus: same.
  • probability theory: degrees of belief.
  • fuzzy logic: also allow degrees of belief.

Propositional Logic: Syntax

• Constants T and F are sentences.
• Any propositional symbol (P, Q, ...) is a sentence.
• If , sentences, so is
  • 
  • (conjunction)
  • (disjunction)
  • (negation)
  • (implication; )
  • (equivalence)
• Rules can be used recursively.

Propositional Logic: Semantics

• T, F have fixed interpretation.
• Interpretation mapping proposition symbols to their meanings.
• Rules for interpreting complex sentences:

  is true iff is true and is true.

  is true iff is true or is true.

  is true iff is not true.

  is true iff is not true or is true.

  is true iff ( is true and is true), or ( is false and is false).

• Rules often expressed using truth tables.
• Implication does not require any causation relation.
• Can use truth tables to test for entailment.

Propositional Logic: Inference Procedure

• Use inference rules to summarise truth table calculations.

  (Instead of , sometimes ).

• Proof: sequence of applications of inference rules, starting with some premise and ending with desired conclusion.
• Common Rules:
  • Modus Ponens (Implication Elimination)
  • And Elimination
  • And Introduction
  • Or Introduction
  • Double Negation Elimination
  • Unit Resolution
  • Resolution

Propositional Logic: Inference Rules (R&N Figure 6.13)

Wumpus in Propositional Logic

• Use propositional symbols like to denote: stench in [1,2].
• Current world state

  
  
  

• Axioms

Find the Wumpus: inference

Problem 1

Look at the following sentences and determine if each is valid, unsatisfiable, or neither, using truth tables or proofs.

1. (Smoke Fire) ( Smoke Fire)
2. Smoke Fire Fire
3. (Smoke Fire) ((Smoke Heat) Fire)

Hint: A sentence is valid if you can prove it. It is unsatisfiable if its negation is valid. If it's neither you can find an assignment of truth values to propositional symbols that makes the sentence false, and another which makes the sentence true.

Problem 1

Problem 2: Description

If the teller had pushed the alarm button, the vault would have locked automatically and the police would have arrived within three minutes. Had the police arrived within three minutes, the robbers' car would have been overtaken. But the robbers' car was not overtaken. Prove the teller did not push the alarm button.

Steps: Write down

• symbols to describe the various propositions.
• the axioms given (3 for this example)
• the axiom that you are required to prove
• each step of proof, indicating what axioms are involved in step, and what inference procedure you are using

Problem 2: Represented in Logic

Let

T:

V:

P:

O:

Axioms

1.  
   
2.  
   
3.  
   

Required to prove:

Problem 2: Proof

First-Order Predicate Calculus

Divide world into:

• objects e.g.
• properties (of objects) e.g.
• relations (between objects)

  e.g.

• (some relations are) functions e.g.
• Examples:
  • ``John is the brother of Susan"
  • ``one plus two equals three"
  • ``Squares neighbouring the wumpus are smelly"
    

Syntax (R&N Figure 7.1)

Notes on syntax

• Sentences represent facts; terms represent objects.
• If x is a variable or a constant, x is a term.
• If , , ..., are all terms and f is an n-ary function symbol, then ) is a term.
• If P is an n-ary predicate and , , ..., are terms, then is a sentence (an atomic sentence).
• If P and Q are sentences, then so is , , , , . (Complex sentences)
• If P is a sentence and x is a variable, then , are sentences.
• universal quantifier, existential quantifier. These can be nested: eats (x, y) and eats (x, y).
• Atomic sentence - no Boolean connectives or quantifiers.
• Literal - atomic formula or its negation.
• Ground literal - literal without variables (also called ``ground term").

Functions vs predicates

• + is a function, used to build terms out of other terms.

  e.g. +(2,2), father-of(David)

• = is a predicate, used to define sentences (which are true or false).

  e.g. =(+(2,2),4), father-of(David,John)

Semantics Again

• Interpretation: mapping between elements of the (formal) language and entities in the world.
• Objects referred to by terms. Claims about objects (properties, relations) expressed by sentences (wffs).
• Usual interpretation: T or F in world.

Semantics (cont.)

• Complex sentences (logical formulas): atomic sentences + logical operators; compositional semantics.
  • Rules for Boolean connectives same as for propositional.
• Universal Quantification:
  • True iff P is true for all objects x in universe.
  • Examples:
    
• Existential Quantification:
• True iff P is true for some object in universe.
• Example:
  

Quantifiers and Equivalences

• Nesting of quantifiers.
  • Eats (s, c)
  • Eats (s, c)
• Equivalences
  • 
  • 
  • 
  • 

The power of FOPC

• Negation:
  • Tall(Jack)
  • Tall(Jack)
  • On(A,B)
• Partial knowledge - disjunction:
  • sister-of(Jan,Sandy) sister-of(Terri,Sandy)

  • Does Sandy have a sister?
    
• Partial knowledge - indefiniteness:

  Above(x,y) w [On(x,w) Above(w,y)]

Reasoning logically

Examples from Discrete Mathematics, H. Matheson (Lewis Carroll)

• Does the conclusion logically follow from the premises P and P'?
  • P: No misers are unselfish.
  • P': None but misers save eggshells.
  • Conclusion: No unselfish people save eggshells.
• What conclusions can you draw from the following three premises, , , ?
  • : Everyone who is sane can do logic.
  • : No insane persons are fit to serve on a jury.
  • : None of your sons can do logic.

Generic logic-based agent (R&N 6.1)

function KB-agent(percept) returns action

static: KB, a knowledge base
t, a counter, initially 0, indicating time

TELL (KB, MAKE-PERCEPT-SENTENCE(percept, t)

action ASK (KB, MAKE-ACTION-QUERY(t)))

TELL (KB, MAKE-ACTION-SENTENCE(action, t)

t t + 1

return action

• Fn TELL ``stores" a new sentence in the KB.
• Function ASK presents a query to the KB (+inference engine) to be proved.
• Percepts, and best actions, must be indexed by time. Percepts recorded as predicates (true if percept at time given)

  percept([stench,breeze,glitter,none,none],3)

• Actions: e.g. turn(right), forward, grab.

  Action query: action(a, 5);

Reflex Agent

• Maps percepts to actions:

  s,b,u,c,t Percept([s,b,Glitter,u,c],t) Action(Grab,t)

• Introduce rules for perception, then use them (introducing bit of internal state)

  s,b,u,c,t Percept([s,b,Glitter,u,c],t) AtGold(t)
  AtGold(t) Action(Grab,t)

• Problems with reflex agents in Wumpus World:
  • When to climb:
  • Can't avoid infinite loops:

Representing change in the world

• Develop internal model of world
  
• Situation Calculus: Useful formalism for representing world that changes over time.
• Identify situations; instead of P(x, ..., x) have P(x, ..., x, s), where s is a situation variable.
• Every property or relation that can change over time is given an extra situation argument; convention: use s and make last argument.
• Examples:

• Time equals state change.

Situation calculus (cont.)

• Actions map situations to situations (R&N Fig 7.3)

  Situation calculus (cont.)

• Examples:

  result(walk-forward-3-steps, s) = s

• Example;

  s at(blackboard,s)
  at(table, result(walk-forward-3-steps,s))

  • Note: all we know is that agent is at the table
• The need to state all the things that don't change as the result of an action; called the Frame Problem.
• Example:
  

The Frame Problem: Blocks World Example

(a)

s x on(x,Table,s)
on(x,Table,result(PutTable(x),s))

(b)

s x y on(x,y,s) y on(x,Table,s)

• (a) and (b) are sufficient to show that
  on(B,Table,S) after a PutTable action.
• But to establish on(A,Table,S) also need a frame axiom.

  s x y z on(x,y,s) x z on(x,y,result(PutTable(z),s)))

Wumpus World: Dynamic axioms

• Relies on Make-Percept-Sequence transforming ``bare" percept sequence into simpler sentences: e.g.
  

Wumpus World: Synchronic Rules

Causal Rules:

model causal connections between properties of world and percepts.

l,l,s at(Wumpus,l,s) adjacent(l,l)
smelly(l)

l,l,s at(pit,l,s) adjacent(l,l)
breezy(l)

Diagnostic:

infer properties of world from perceptual information.

l,s smelly(l) at(Wumpus,l,s)
(adjacent(l,l) l=l)

l,s breezy(l) at(pit,l,s)
adjacent(l,l)

Miscellaneous

• Wumpus World: Keeping Track of Location
  • Initial location: at(Agent, [1,1], S)
  • Direction: Orientation(Agent,S)
  • Adjacent, Wall, etc: see text.
  • What's a safe location?

x,s at(Wumpus,x,s) pit(x) ok(x)

• More on actions:
  • May want to ascribe particular value to different actions:
  • Rather than just reacting, may want to plan ahead a whole sequence of actions.

The Frame Problem

Inferential:

more things stay the same than change, but have to continue drawing inferences about things that stay the same.

In planning, will look at special action-oriented representations that avoid this (less expressive than FOPC).

Representational:

Proliferation of frame axioms (essentially one for each property an action does not affect).

Handling the Representational Frame Problem

Modify the logic:

• make predicate without situation argument into a term (``reify", p.230)
• introduce new predicate holds:

  at(blackboard, s) becomes

  holds(at(blackboard),s)

• at(blackboard) now property-object of being at blackboard.
• Can write a more general frame axiom

p,s,x holds(p,s) p at(x)

holds(p,result(walk-forward-3-steps,s)).

Relatives of The Frame Problem

Ramification Problems:

Specifying and inferring all the things that do change.

Example 1: When I walk forward three steps:

Example 2: Move table:

Qualification Problem:

Specifying and checking all the preconditions of an action. Example 3: Grabbing a gold brick.

Wumpus World Again

Some modified examples of axioms using the holds predicate.

• General Rules:

s holds(glitter,s)
holds(have(gold), result(grab,s))

sx holds(have(x),result(release,s))

• A Frame Axiom:
  

a,x,s holds(have(x),s) a release

holds(have(x),results(a,s))

Wumpus World Examples (cont.)

Causal Rules:

if the world is a certain way...

l,l,s holds(at(Wumpus,l),s)
adjacent(l,l) smelly(l)

l,l,s holds(at(pit,l),s)
adjacent(l,l) breezy(l)

Diagnostic:

if some consequence is true...

l,s smelly(l) holds(at(Wumpus,l)s)
(adjacent(l,l) l=l)

l,s breezy(l) holds(at(pit,l),s)
adjacent(l,l)

Substitution

• Have to talk about substituting particular individuals for the variables.
• Notation:

  subst(, ) denotes the result of applying the substitution (or binding list) to sentence .

  where is a list v/t, ..., v/t that specifies what terms (the t) replace what variables (the v).

Example 1:

subst({x/fish,y/jo}, eats(y, x))

= eats(jo,fish)

where = {x/fish,y/jo}, = Likes(x, y).

New Inference Rules for FOPC

• Existential
  • Elimination ()

    where v is a variable in and k is a constant not in or elsewhere in the KB.
    

    e.g. :

    (Sometimes called Skolemisation)

  • Introduction ()

    
    

    where v does not occur in , and g is a ground term that does.
    

    e.g.

New Inference Rules for FOPC (cont)

• Universial
  • Elimination ()

    

    where v is a variable in , and g is a ground term.
    

    e.g.
    

  • Introduction ()

    

    where v appears free in . (We won't use this)

Automating the proof procedure?

• Relationship to search
  • start state = conjunction of axioms in the KB
  • operators = inference rules
  • goal state = theorem
• Problem: big branching factor, lots of rules, lots of ways to apply some rules.
• So need a better search space; try to combine into a single, more general rule...

Generalised modus ponens

• Combines , , and .
  

P(d), Q(d), x P(x) Q(x) R(x)

R(d)

• For atomic sentences p, p' and ,

  where there is a substitution so that

  subst(,p') = subst(,p), for all i:
  

  p',p',...,p',(p p,...p q)

  subst(, q)

Generalised Modus Ponens: Example

x {person(x) lives-in-melbourne(x) footy-fan(x)}

person(annn)

lives-in-melbourne(annn)

= {x/annn}

Conclusion:

subst({x/annn},footy-fan(x))=footy-fan(annn)

Unification

• The process of finding the substitution is unification.
• The substitution itself is a unifier.
• Process helps focus search on substitutions that matter.
• unify takes two atomic sentences p and q and returns a substitution that makes them look the same.

unify(p,q)= where subst(,p)=subst(,q).

Unification Examples

• Illustrate unify by example (see text for detailed algorithm):

unify(P(a,x),P(a,b)) = {x/b}

unify(P(a,x),P(y,b)) = {x/b,y/a}

unify(P(a,x),P(y,f(y)) = {y/a,x/f(a)}

unify(P(a,x),P(x,b)) = failure (a b)

To avoid such problems, standardise variables apart. Replace x with x in P and x with x in Q. Then:

unify(P(a,x),P(x,b)) = {x/b, x/a}

• Not everything can be unified:

unify(P(a,b),P(x,x)) = failure

unify(P(a,f(a)),P(x,x)) = failure

• Most General Unifier (mgu): See text.

Use of Generalised Modus Ponens

• Forward-chaining: start with axioms, generate conclusions, working to get new consequences or to goal.
• Backward-chaining: start with goal, find implications that would allow you to prove it, working back to axioms.
• Generalised Modus Ponens is not complete. For example:

  1.

  x P(x) Q(x)

  2.

  x P(x) R(x)

  3.

  x Q(x) S(x)

  4.

  x R(x) S(x)

• Conclude S(a) for any a, but no way to conclude this with generalised MP. (Intuitively: no way to ``relate" 1 and 2.)
• Modus Ponens can derive new atomic conclusions, but not new implications.

Soundness and Completeness (again)

• Soundness.

  An inference rule is sound if it produces only WFFs that are true in all interpretations in which the original set of WFFs were ture.

  If KB W, then KB W (provable is true)

• Completeness

  A set of inference rules is complete if it can produce any WFF that is true in all interpretations in which the original set of WFFs is true.

  If KB W, then KB W (true is provable)

Completeness of FOPC?

• Godel's completeness theorem shows that there is a set of inference rules R for FOPC so that:

  If KB , then KB

• There is an inference procedure that will return true if a sentence is true.
• FOPC entailment is semidecidable.
• Complete inference procedure for FOPC found by Robinson 35 years after Godel's result: resolution.
• Resolution can (more or less) easily be automated, and can derive implications (so more powerful than MP).

General Resolution Rule

• General Case, (where disjuncts may not be ground)
• Need to unify the complimentary literals (i.e. UNIFY(, ) = ) and apply unifying substitution to the rest of the resolvent.

  p ... p ... p,

  q ... q ... q

  subst(,p...pp...p

  q...qq...q)

Refutation Proofs

• We want to refute the negation of the purported theorem.
• Example:

  (1) Cats like fish.
  

  (2) Cat eat everything they like
  

  (3) Josephine is a cat.
  

  Prove: Josephine eats fish.
  

  Refutation: suppose ``Josephine does not eat fish" and get a contradiction.
  

• In practice, negate goal, add it to set of axioms, derive a contradiction.

Refutation Proofs

• Given some consistent set of axioms S, to show that S W, show that (S {W}) is unsatisfiable.
• Why refutation proofs work:
  1. S W: every interpretation I that satisfies S, satisfies W.
  2. Any interpretation I satisfies either W or W (but not both).
  3. No interpretation satisfies S and W satisfies S satisfies W [from 1]
     does not satisf W [from 2]
     i.e. (S {W}) is unsatisfiable.
  4. Resolution is sound and complete:
• Resolution can establish W is entailed by the KB, but can't generate all logical consequences of a set of WFFs.

Converting WFFs to CNF

1. Eliminate implication symbols.
2. Reduce scopes of negation symbols. Convert:
   • (p q) to p q
   • (p q) to p q
   • xp to xp
   • p to p
   • p to p
3. Standardize variables: convert

   x p(x) x Q(x) to

4. Move all universal quantifers to the front.
   

   Converting WFFs to CNF (cont.)

5. Eliminate existential quantifiers (Skolemize).
6. Eliminate universal quantifiers.
   
7. Distribute over .
   
8. Flatten nested conjuncts and disjuncts (now in CNF).

Refutation proof example

Resolution Example

1. If a course is easy, there are some students that are enrolled in it who are happy.
2. If a course has a final exam, no students that are enrolled in it are happy.
3. If a course has a final exam, the course is not easy.

• Step 1: Using only the predicates HAS-FINAL, EASY, HAPPY, and ENROLLED represent these statement as predicate calculus formulas.
• Step 2: Convert these statements to clauses.
• Step 3: Use Resolution to prove statement (3).

Example

Resolution won't always yield an answer:example

KB

WORLDS

MODELS

M1: Dick is Deb's brother.

M2: Dick is David's father.

W3 is true in model M1, but not in M2.

Miscellaneous

• Control Strategies for Resolution
  • A strategy is complete if its use results in a procedure that will find a contradiction (eventually) whenever one exists.
  • See Text (pp284-285)for description of various control strategies.
• How is Prolog (a programming language) related to FOPC theorem proving?
  • Restrict to Horn clauses (one positive literal); Horn clause logic is decidable.
  • Linear-input resolution, depth-first search, desolve on left-most literal
  • Typically order clauses and rules to avoid some search problems.

Summary

• Revised syntax and semantics of propositional logic and the predicate calculus.
• Can define an agent that reasons using first-order logic. It needs to
  • Percepts abstract descr. of current state;
  • Maintain internal model of world;
  • Express/use info on desirability of actions;
  • Goals + knowledge about actions plans.
• Knowledge about actions and effects can be represented using situation calculus.
• Choice between: Diagnostic rules (percepts propositions); Causal rules (describe world percepts).
• Extension to propositional inference rules allows construction of proofs for FOPC. However branching factors prohibitive.
• The use of unification to identify appropriate substitutions for variables eliminates the instantiation step in proofs, making process much more efficient.
• A generalised version of Modus Ponens uses unification to provide a natural and powerful inference rule. Can be used in forward and backward chaining.
• The generalized resolution inference rule provides a complete system for proof by refutation.
• Resolution proof by refutation requires a normal form, but any sentence can be put into the form.

 
• About this document ...