kr - ch1, 2

http://users.skynet.be/bs661306/peter/doc/hpv00r03-841.htm
KR (Knowledge Representation) Hypothesis (Smith 1982):
1. there's some structural ingredients to represent knowledge -- knowledge base
2. there's some process to manipulate these ingredients via inference -- reasoning

Notes; Exist structures that:
• we can interpret propositionally
• determine how the system behaves

eg. Expert system, GPS
http://en.wikipedia.org/wiki/General_Problem_Solver
General Problem Solver (GPS) was a computer program created in 1957 by Herbert Simon, J.C. Shaw, and Allen Newell intended to work as a universal problem solver machine. Any formalized symbolic problem can be solved, in principle, by GPS. For instance: theorems proof, geometric problems and chess playing. It was based on Simon and Newell's theoretical work on logic machines. GPS was the first computer program which separated its knowledge of problems (rules represented as input data) from its strategy of how to solve problems (a generic solver engine).


reasoning - Manipulation of symbols encoding propositions to produce representations of new propositions

representation - symbols standing for things in the world

knowledge - taking the world to be one way and not the other, propositions, eg. I know that the sky is blue

entails - eg kb entails alpha, so if the world satisfies kb then it must also (implied that it) satisfy alpha

inference - process of calculating entailments

sound - get only entailments

complete - get all entailments

the language of first order logic

wffs - well-formed formula, St(Bob) V St(Sue) is wff but St(Bob V Sue) is not wff

abbrevations:
logical symbols:
(α ⊃ β) for (¬α ∨ β)
(α ≡ β) for ((α⊃β) ∧ (β⊃α))

x ⊃ y means x -> y means if x then y

non-logical symbols: predicates, functions

a sentence: wff with no free variables (closed)

Substitution: α[v/t] means α with all free occurrences of the v replaced by term t
free occurrence (no scope - ∃ and ∀)

interpretation - Each interpretation assigns to function f a mapping from objects to objects. ℑ = 〈 D, I 〉, D is the domain of discourse (eg people, table), I is an interpretation mapping (eg prop symbols -> true, false)

satisfaction
will write as ℑ,µ = α “α is satisfied by ℑ and µ”
where µ ∈ [Variables → D], as before
or ℑ = α, when α is a sentence
“α is true under interpretation ℑ”
or ℑ = S, when S is a set of sentences

Entailment defined
S |= α iff for every ℑ , if ℑ |= S then ℑ |= α.
Say that S entails α or α is a logical consequence of S:
In other words: for no ℑ , ℑ |= S ∪ {¬α}. S ∪ {¬α} is unsatisfiable

“the elements of S are true under interpretation ℑ”

S = KB = Knowledge base

Special case when S is empty: |= α iff for every ℑ , ℑ |= α.
Say that α is valid. (p.30)

***
include such connections explicitly in S
Key idea ∀x[Dog(x) ⊃ Mammal(x)]
of KR: the rest is just
Get: S ∪ {Dog(fido)} |= Mammal(fido) details...

p33. proof by interpretation, if S |= alpha then I |= S and I= alpha
case1. I |= Green(b), show I |= Green(b) ∧ ¬Green(c) ∧ On(b,c). (based on S, so entailed)
case2. I |= ~Green(b), show I |= Green(a) ∧ ¬Green(b) ∧ On(a,b). (based on S, so entailed)

if I |= alpha, then I is a model of alpha

eg. soap opera world - domains
individuals: john, sleezyTown
basic types: Place, Person
relationships / functions: MarriedTo, DaugherOf

facts = terms
Man(john)
Rich(john)

∀y[Woman(y) ∧ y ≠ jane ⊃ Loves(y,john)]

x ⊃ y means x -> y means if x then y
attributes: Rich, Beautiful

closure: ∀x[Person(x) ⊃ x=jane ∨ x=john ∨ x=jim ...]

Denotation p27
||t||i,u where u in [variables -> d]

Clausal representation p48
Formula = conjunction ^ of clauses { [p, r, s], [p, r, s], [ p ] }
Clause = disjunction V of literals [p, r, s]
Literal = atomic sentence or its negation p
positive literal and negative literal

Resolvent
clauses [w, r, q] and [w, s, ~r] have [w, q, s] as resolvent wrt r.

Resolution is refutation complete

Resolution p53. (uses the process of derivations)
To determine if KB |= a,
1. put KB, ~a into CNF to get S
2. if S->[], the KB V ~a is unsatisfiable and so KB |= a
3. otherwise, KB V ~a is satisfiable and so KB does not entail a

ground if literal contains NO variables eg. Wife(bob,marry)

Generalizing CNF p.57
Generalizing CNF
Resolution will generalize to handling variables
But to convert wffs to CNF, we need three additional steps:
1. eliminate É and º
2. push Ø inward using also Ø"x.a ß $x.Øa etc.
3. standardize variables: each quantifier gets its own variable
e.g. $x[P(x)] Ù Q(x) ß $z[P(z)] Ù Q(x) where z is a new variable
4. eliminate all existentials (discussed later)
5. move universals to the front using ("xa) Ù b ß "x(aÙ b)
where b does not use x
6. distribute Ú over Ù
7. collect terms
Get universally quantified conjunction of disjunction of literals

Answer predicate - A(x)
[~St(x), ~Happy(x), A(x)]
...
[A(bob)]

Skolem - names for individuals claimed to exist, called Skolem

Skolem preserve satisfiability, not equivalence so ExP(x) not equal P(a)!!

*MGU - most general unifier p70. / unification
- finding skolem variables theta given P(f(x), y, g(y)) and P(f(x), z, g(x)), answer is theta = {y/z, z/x} to get P(f(x), x, g(x))

***Note: important to get dependence of variables correct p65
AyExR(x,y) => AyR(f(y),y) so the best way to remember is to put brackets, it's better Ax (for all x) is inside the bracket because it's more flexible
vs. ExAyR(x,y) => AyR(a,y)

strategies:
- directional connectives (forward, backward)
- unit clauses
- set of support (always resolve with at least one clause that's the ancestor of ~q, just unifying with KB is useless)
- clause elimination, tautology (always true), pure clause (only one atom p in the formula)

horn clause = has at MOST one +ve literal (p80)
- as implications: (¬child ∨ ¬male ∨ boy)
- e.g. [¬p1, ¬p2, ..., ¬pn, q]
- e.g. [¬p1, ¬p2, ..., ¬pn] and also [ ] (all negative)
- p1 ∧ p2 ∧ ... ∧ pn ⇒ q (if p1 and p2 and ... and pn then q) or Note:
(¬p1 ∨ ¬p2 ∨ ... ∨ ¬pn ∨ q) or [(p1 ∧ p2 ∧ ... ∧ pn) ⊃ q]

SLD - (Selected literals) (linear form) (definite clauses)
sld derivation / resolution in Horn clauses - can also use a goal tree where the root is the goal and leaves are in the KB

back-chaining - depth first, left-right, back-chaining (strategy used in Prolog), can go to inf. loop

forward-chaining - mark atoms as solved

problem - can give inf. branch of resolvents in FOL

Standardize variables: each quantifier should use a different one

Ordering goals p94.
1. get ParentOf(sam,z): find child of Sam searching downwards
2. get ParentOf(z,sue): find parent of Sue searching upwards
3. get ParentOf(–,–): find parent relations searching in both directions
Search strategies are not equivalent
if more than 2 children per parent, (2) is best