Intelligent Systems Lecture Notes

23 September 2011 • Reasoning

---

Outline

• Queries
• Proofs
  • Proof algorithms.
  • Top-down and bottom-up.

Queries

• A query is a conjunct of atoms (a body).

  ask \(a_1\) \(\wedge\) \(\ldots\) \(\wedge\) \(a_n\)

• A query has value true or unknown relative to a knowledge base and an interpretation.
• Consider, for the moment, single-atom queries.

  ask grassisgreen

Answering Atomic Queries.

• If the query atom is a definite clause in the knowledge base, the interpretation gives the result.

  KB: { a, b }, I: { a }

  ask a ⇒ true

  ask b ⇒ unknown

Answering Atomic Queries..

• What happens if the query atom is the head of a rule?

  KB: { a \(\leftarrow\) b \(\wedge\) c }, I: { \(\cdots\) }

  ask a ⇒ ?

• If the atom is given in the interpretation, the answer's easy.
• If it's not, we need more machinery.

Proofs

• Formally, answering a query involves determining if a proposition (a conjunction) logically follows from a knowledge base.
  • This is known as deduction, a form of inference.
• A proof procedure is an algorithm that determines what propositions logically follow from a knowledge base.
  • A successful result is a demonstration of how a proposition follows from a knowledge base.

Atomic Reasoning

• If an atom a is true in a knowledge base, then the result of query a is “yes”.
• If atoms a and b are true, then the queries

  a
  b
  a \(\wedge\) b

  all return “yes”.
• The set of all true atoms in a knowledge base can be used to answer queries.

Atoms and Queries

• Let T be all true atoms in a knowledge base and q be a query.
• If every atom in q is also in T, then q returns “yes”.

  T: { a, b, c }, ask a \(\wedge\) c ⇒ yes

• If some atom in q is not in T, then q returns “unknown”.

  T: { a, b, c }, ask a \(\wedge\) d ⇒ unknown

Bottom-Up Proof Procedure

• A bottom-up proof determines what can be proved by starting with atoms and working up.

  BUProve(KB)
  
    proved = { }
  
    repeat
      select h ← b1 ∧ … ∧ bn in KB
      where bi ∈ proved and h ∉ proved
      proved U= { h }
    until nothing more to select
  
    return proved

BUProve Example

select h ← b1 ∧ … ∧ bn in KB
where bi ∈ proved and h ∉ proved
proved U= { h }

KB		proved
a \(\leftarrow\) b \(\wedge\) c b \(\leftarrow\) d \(\wedge\) e b \(\leftarrow\) g \(\wedge\) e c \(\leftarrow\) e d e f \(\leftarrow\) g \(\wedge\) a		{ } { d } { d, e } { c, d, e } { b, c, d, e } { a, b, c, d, e }

BUProve Results

• BUProve(KB) returns all atoms that logically follow from KB.
• Only queries containing only atoms from BUProve() return yes.

  { a, b, c, d, e } = BUProve(KB)

  ask a ⇒ yes
  ask a \(\wedge\) d ⇒ yes
  ask f ⇒ unknown
  ask a \(\wedge\) f ⇒ unknown
  

BUProve Rationale.

• Why is

  select h ← b1 ∧ … ∧ bn in KB
  where bi ∈ proved and h ∉ proved
  proved U= { h }
  

  justified?

• In other words,

  If h \(\leftarrow\) b exists and b is true, why is h true?

BUProve Rationale..

h ← b t t t t t f f f t f t f

If h \(\leftarrow\) b is true and b is true, then h must be true too. This reasoning rule is known as modus ponens.

• Get the direction right: if h \(\leftarrow\) b and h are true, it is not necessary that b is true.

  if dogissmelly \(\leftarrow\) dogiswet is true
  and dogissmelly is true
  then ...

The Other Direction

• Suppose query a \(\wedge\) b is given for a knowledge base containing

  a \(\leftarrow\) c \(\wedge\) d

• From the rule, a is true when c \(\wedge\) d is true.
• By substitution, the query c \(\wedge\) d \(\wedge\) b is equivalent to the query a \(\wedge\) b.
• If the knowledge base contains the definite clause a, then a is true.
  • The query a \(\wedge\) b is equivalent to b.

Top-Down Proof Procedure

TDProve(KB, query)

  atoms = query

  repeat
    select atom a in atoms
    choose definite clause a ← B in KB
    atoms U= atomsIn(B)
  until atoms = { }

  return yes

TDProve Example

select atom a in atoms
choose definite clause a ← B in KB
atoms U= atomsIn(B)

KB		atoms	atoms
a \(\leftarrow\) b \(\wedge\) c b \(\leftarrow\) d \(\wedge\) e b \(\leftarrow\) g \(\wedge\) e c \(\leftarrow\) e d e f \(\leftarrow\) g \(\wedge\) a		{ a } { b, c } { d, e, c } { e, c } { c } { e } { }	{ a } { b, c } { g, e, c } { g, c } { g, e } { g }

TDProve Rationale.

• What justifies

  select atom a in atoms
  choose definite clause a ← B in KB
  atoms U= atomsIn(B)
  

• In other words,

  If I want to prove h true
  and I know h \(\leftarrow\) b is true
  then can I prove b is true instead?

TDProve Rationale..

• From the truth table:

  h ← b t t t t t f f f t f t f

  If I know h \(\leftarrow\) b is true and I know b is true then h must be true too. Via modus ponens.

Knowledge Bases and Truth

• Both the bottom-up and top-down rationales assume definite clauses in a knowledge base are true.
  • For example, modus ponens requires true rules.
• An interpretation determines the logical values of definite clauses in a knowledge base.
• A model is an interpretation which causes every definite clause in a knowledge base to be true.
• Every propositional knowledge base has a model.

Algorithms and Proofs

• If a reasoning algorithm can establish a query q for knowledge base KB, the algorithm has proved (or derived) q.
  • Represented as \(KB\vdash q\).
• If a proposition p is true under all models of KB, then p is a logical consequence of KB.
  • Or p logically follows from KB, or KB entails p.
  • Represented as \(KB\models p\).

Derivation and Entailment

• How do derivation and entailment relate?
• A sound proof algorithm proves only propositions entailed by the knowledge base.
  • If \(KB\vdash q\) then \(KB\models q\)
  • Everything proved is true.
• A complete proof algorithm can prove every entailed proposition.
  • If \(KB\models q\) then \(KB\vdash q\)
  • Everything is true is provable.

Summary

• A query is a conjunction of atoms.
• A query q may be true relative to a knowledge base KB.
  • q is a logical consequence of KB, \(KB\vdash q\).
• A proof procedure finds the logical consequences of a knowledge base.
  • Working top-down from the query or bottom-up from the atoms.

References

• Resolution (Chapter 4) in Knowledge Representation and Reasoning by Ronald Brachman and Hector Levesque, Morgan Kaufmann, 2004.
• From Logic-Based Chaining to Production Systems (Chapter 6) in Intelligent Systems by Robert Schalkoff, Jones and Bartlett, 2011.
• Inference in First-Order Logic (Chapter 9) in Artificial Intelligence, A Modern Approach, third edition, by Stuart Russell and Peter Norvig, Prentice Hall, 2010.

Credits

---

This page last modified on 2011 September 23.