Kecerdasan Buatan (KI092301)
Inference First Order Logic Chastine Fatichah Teknik Informatika Institut Teknologi Sepuluh Nopember November 2012 12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
1
Pokok Bahasan • Mengubah First Order Logic ke Propotional • • • • • •
Logic Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution Ringkasan
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
2
Sejarah Reasoning • • • • • • • • • • •
450b.c. Stoics 322b.c. Aristotle 1565 Cardano 1847 1879 1922 1930 1930 1931 1960 1965
12/10/2012
propositional logic, inference “syllogisms" (inference rules), quantifiers probability theory (propositional logic + uncertainty) Boole propositional logic (again) Frege logic Wittgenstein proof by truth tables Gӧdel complete algorithm for FOL Herbrand complete algorithm for FOL (reduce to propositional) Gӧdel complete algorithm for arithmetic Davis/Putnam “practical" algorithm for propositional logic Robinson “practical" algorithm for FOL resolution Inference First Order Logic @ Kecerdasan Buatan (KI092301)
3
Pokok Bahasan • Mengubah First Order Logic ke Propotional • • • • • •
Logic Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution Ringkasan
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
4
Universal instantiation (UI) Semua kalimat dengan universal quantifier () meng-entail semua instantiation-nya: v α Subst({v/g}, α) untuk sembarang variabel v and ground term g Contoh x King(x) Greedy(x) Evil(x) meng-entail: King(John) Greedy(John) Evil(John) King(Richard) Greedy(Richard) Evil(Richard) King(Father(John)) Greedy(Father(John)) Evil(Father(John)) 12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
5
Existential instantiation (EI) Untuk sembarang kalimat α, variabel v, and konstanta k yang tidak muncul di knowledge-base: v α Subst({v/k}, α) Contoh x Crown(x) OnHead(x,John) meng-entail: Crown(C1) OnHead(C1,John) Dengan syarat C1 adalah konstanta baru, disebut konstanta Skolem
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
6
Existential instantiation (EI) • Universal instantiation bisa digunakan berkali•
• •
kali untuk menambahkan kalimat baru. KB yang baru logically equivalent dengan yang lama. Existential instantiation cukup digunakan sekali untuk menggantikan kalimat existential. KB yang baru tidak logically equivalent dengan yang lama, tetapi satisfiable iff KB yang lama juga satisfiable inferentially equivalent
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
7
Mengubah ke Propositional Inference Misalkan KB berisi kalimat-kalimat berikut: x King(x) Greedy(x) Evil(x) King(John) Greedy(John) Brother(Richard,John)
Dan jika kita mengambil semua kemungkinan instantiation dari kalimat universal, maka kita dapatkan KB sbb: King(John) Greedy(John) Evil(John) King(Richard) Greedy(Richard) Evil(Richard) King(John) Greedy(John) Brother(Richard,John)
KB yang baru disebut propositionalized: proposition symbolnya adalah: King(John), Greedy(John), Evil(John), King(Richard), dll. 12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
8
Mengubah ke Propositional Inference • • • •
Klaim : Setiap FOL KB dapat di propositional kan sebagai entailment Klaim: Kalimat ground di entail dengan KB baru jika dan hanya jika entail terhadap original KB Idea: propositionalize KB dan query, lalu gunakan resolution Problem: dengan adanya function, ground terms menjadi infinite.
•
Contoh: Father(Father(Father(John)))
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
9
Masalah dengan propositionalization •
Propositionalization menghasilkan banyak kalimat irrelevant.
•
Contoh:
x King(x) Greedy(x) Evil(x) King(John) y Greedy(y) Brother(Richard,John)
manusia bisa cepat mengerti kalau Evil(John), namun propositionalization menghasilkan: King(Richard) Greedy(Richard) Evil(Richard) Greedy(Richard)
yang irrelevant
•
Dengan p predicate k-ary dan n constant, ada p x nk instantiation!
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
10
Pokok Bahasan • Mengubah First Order Logic ke Propotional • • • • • •
Logic Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution Ringkasan
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
11
Unification •
Inference : Substitution θ sedemikian hingga King(x) dan Greedy(x) cocok dengan King(John) dan Greedy(y)
θ = {x/John,y/John}
•
Unify(α,β) = θ jika αθ = βθ p q Knows(John,x) Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
12/10/2012
θ
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
12
Unification •
Inference : Substitution θ sedemikian hingga King(x) dan Greedy(x) cocok dengan King(John) dan Greedy(y)
θ = {x/John,y/John}
•
Unify(α,β) = θ jika αθ = βθ p q Knows(John,x) Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
12/10/2012
θ {x/Jane}}
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
13
Unification •
Inference : Substitution θ sedemikian hingga King(x) dan Greedy(x) cocok dengan King(John) dan Greedy(y)
θ = {x/John,y/John}
•
Unify(α,β) = θ jika αθ = βθ p q Knows(John,x) Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
12/10/2012
θ {x/Jane}} {x/OJ,y/John}}
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
14
Unification •
Inference : Substitution θ sedemikian hingga King(x) dan Greedy(x) cocok dengan King(John) dan Greedy(y)
θ = {x/John,y/John}
•
Unify(α,β) = θ jika αθ = βθ p q Knows(John,x) Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
12/10/2012
θ {x/Jane}} {x/OJ,y/John}} {y/John,x/Mother(John)}}
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
15
Unification •
Inference : Substitution θ sedemikian hingga King(x) dan Greedy(x) cocok dengan King(John) dan Greedy(y)
θ = {x/John,y/John}
•
Unify(α,β) = θ jika αθ = βθ p q Knows(John,x) Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)
θ {x/Jane}} {x/OJ,y/John}} {y/John,x/Mother(John)}} {fail}
• Standardizing apart variable menghilangkan overlap, contoh Knows(z17,OJ) 12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
16
Pokok Bahasan • Mengubah First Order Logic ke Propotional • • • • • •
Logic Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution Ringkasan
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
17
Generalized Modus Ponens (GMP) Inference Rule GMP
p1', p2', … , pn', ( p1 p2 … pn q) dimana pi'θ = pi θ untuk semua i
p1' is King(John) p2' is Greedy(y) θ is {x/John,y/John} q θ is Evil(John)
• •
qθ
p1 is King(x) p2 is Greedy(x) q is Evil(x)
GMP dengan KB yang berisi definite clauses: p1 p2 … pn q Semua variabel diasumsikan universally quantified
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
18
Soundness pada GMP •
Perlu menunjukkan bahwa p1', …, pn', (p1 … pn q) ╞ qθ dimana pi'θ = piθ untuk semua i
•
Lemma: Untuk setiap definite clause p, terdapat p ╞ pθ dengan Universal instantiation (UI) 1. (p1 … pn q) ╞ (p1 … pn q)θ = (p1θ … pnθ qθ) 2. p1', …, pn' ╞ p1' … pn' ╞ p1'θ … pn'θ 3. Dari 1 dan 2, qθ mengikuti Modus Ponens
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
19
Contoh Knowledge Base “ The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American. “
Buktikan bahwa Colonel West is a criminal !!
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
20
Contoh Knowledge Base •
... it is a crime for an American to sell weapons to hostile nations: American(x) Weapon(y) Sells(x,y,z) Hostile(z) Criminal(x)
•
Nono … has some missiles: x Owns(Nono,x) Missile(x): Owns(Nono,M1) and Missile(M1)
•
… all of its missiles were sold to it by Colonel West Missile(x) Owns(Nono,x) Sells(West,x,Nono)
•
Missiles are weapons: Missile(x) Weapon(x)
•
An enemy of America counts as "hostile“: Enemy(x,America) Hostile(x)
•
West, who is American … American(West)
•
The country Nono, an enemy of America … Enemy(Nono,America)
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
21
Pokok Bahasan • Mengubah First Order Logic ke Propotional • • • • • •
Logic Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution Ringkasan
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
22
Forward chaining FOL dengan GMP Algoritma forward chaining
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
23
Contoh Forward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
24
Contoh Forward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
25
Contoh Forward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
26
Forward chaining properti • • • •
Sound dan complete untuk first-order definite clauses Datalog = first-order definite clauses + tanpa function Time complexity FC pada Datalog polynomial Tapi pada kasus umum, bisa infinite loop kalau tidak dientail. Proses pattern matching pada premise NP-hard.
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
27
Pokok Bahasan • Mengubah First Order Logic ke Propotional • • • • • •
Logic Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution Ringkasan
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
29
Backward chaining FOL dengan GMP Algoritma backward chaining
SUBST(COMPOSE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p)) 12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
30
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
31
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
32
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
33
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
34
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
35
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
36
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
37
Contoh Backward chaining FOL
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
38
Backward chaining properti • Depth-first search: • • •
linear space complexity incomplete (infinite loops) inefficient (repeated subgoals)
• Prinsip dasar logic programming
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
39
Logic programming: Prolog Logic programming 1. Identify problem 2. Assemble information 3. Tea break 4. Encode information in KB 5. Encode problem instance as facts 6. Ask queries 7. Find false facts
Ordinary programming Identify problem Assemble information Figure out solution Program solution Encode problem instance as data Apply program to data Debug procedural errors
(Harusnya) lebih mudah men-debug Capital(NewYork;US) daripada x = x + 2 !
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
40
Prolog • Appending two lists to produce a third: append([],Y,Y). append([X|L],Y,[X|Z]) :- append(L,Y,Z). • query: • answers: •
append(A,B,[1,2]) ? A=[] B=[1,2] A=[1]
B=[2]
A=[1,2] B=[]
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
41
Konversi ke CNF • Everyone who loves all animals is loved by someone:
x [y Animal(y) Loves(x,y)] [y Loves(y,x)]
• 1. Eliminasi biconditionals dan implikasi
x [y Animal(y) Loves(x,y)] [y Loves(y,x)]
• 2. Pindah inwards: x p ≡ x p, x p ≡ x p x [y (Animal(y) Loves(x,y))] [y Loves(y,x)] x [y Animal(y) Loves(x,y)] [y Loves(y,x)] x [y Animal(y) Loves(x,y)] [y Loves(y,x)]
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
42
Konversi ke CNF. 3.
4.
Standarisasi variabel:
x [y Animal(y) Loves(x,y)] [z Loves(z,x)]
Skolemize: bentuk umum pada existential instantiation. Setiap variabel existential diganti dengan Skolem function pada universally quantified variables:
x [Animal(F(x)) Loves(x,F(x))] Loves(G(x),x)
5.
6.
Hapus semua universal quantifiers:
[Animal(F(x)) Loves(x,F(x))] Loves(G(x),x)
Distribusi over :
[Animal(F(x)) Loves(G(x),x)] [Loves(x,F(x)) Loves(G(x),x)]
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
43
Resolution proof: definite clauses
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
44
Sumber : 1.Slide perkuliahan Stuart Russell's (Berkeley) http://aima.cs.berkeley.edu/ 2.Slide perkuliahan Sistem Cerdas Ruli Manurung (Universitas Indonesia) http://www.cs.ui.ac.id/WebKuliah/IKI30320/
12/10/2012
Inference First Order Logic @ Kecerdasan Buatan (KI092301)
45
