IKI 30320: Sistem Cerdas Kuliah 13: Inference in FOL

IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification

IKI 30320: Sistem Cerdas Kuliah 13: Inference in FOL

Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Ruli Manurung Fakultas Ilmu Komputer Universitas Indonesia

5 November 2007

Outline IKI30320 Kuliah 13 5 Nov 2007

1

Mengubah FOL ke PL

2

Unification

3

Inference Rule untuk FOL

4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan

Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining

Ringkasan


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Ide tahun 60-an IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Kita sudah melihat mekanisme inference untuk propositional logic Inference rule: Modus Ponens Normal form: Horn clause Algoritma: Forward chaining, Backward chaining Inference rule: Resolution Normal form: CNF Algoritma: Proof-by-contradiction

Pendekatan-pendekatan ini sound dan complete.

Ide tahun 60-an IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining

Kita sudah melihat mekanisme inference untuk propositional logic Inference rule: Modus Ponens Normal form: Horn clause Algoritma: Forward chaining, Backward chaining Inference rule: Resolution Normal form: CNF Algoritma: Proof-by-contradiction

Pendekatan-pendekatan ini sound dan complete.

Logic programming Resolution Ringkasan

Cara mudah melakukan inference FOL: Jika KB dan query dalam FOL bisa diterjemahkan ke dalam PL, beres!

Instantiation IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification

Ground term: sebuah term tanpa variable, mis: Ani, Ayah(Anto), 2007 Instantiation: kalimat di mana sebuah variable diganti dengan sebuah ground term (diperoleh dengan mengaplikasikan sebuah substitution)


Contoh α = ∀ x mahasiswa(x, FasilkomUI) ⇒ pintar (x) β = ∃ x mahasiswa(x, Gundar ) ∧ pintar (x) σ = {x/Anto} S UBST(σ, α) menghasilkan instantiation:




Contoh α = ∀ x mahasiswa(x, FasilkomUI) ⇒ pintar (x) β = ∃ x mahasiswa(x, Gundar ) ∧ pintar (x) σ = {x/Anto} S UBST(σ, α) menghasilkan instantiation: mahasiswa(Anto, FasilkomUI) ⇒ pintar (Anto) S UBST(σ, β) menghasilkan instantiation:




Contoh α = ∀ x mahasiswa(x, FasilkomUI) ⇒ pintar (x) β = ∃ x mahasiswa(x, Gundar ) ∧ pintar (x) σ = {x/Anto} S UBST(σ, α) menghasilkan instantiation: mahasiswa(Anto, FasilkomUI) ⇒ pintar (Anto) S UBST(σ, β) menghasilkan instantiation: mahasiswa(Anto, Gundar ) ∧ pintar (Anto)

Universal Instantiation IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

Sebuah kalimat dengan universal quantifier (∀) meng-entail semua instantiation-nya: ∀v α SUBST ({v /g},α)

Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

untuk sembarang variable v dan 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)) .. .

Existential Instantiation IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL

Untuk sembarang variable v , kalimat α dan constant k yang tidak muncul di knowledge-base: ∃v α SUBST ({v /k },α)

Forward chaining

Contoh

Backward chaining

∃ x Crown(x) ∧ OnHead(x, John) meng-entail: Crown(C1 ) ∧ OnHead(C1 , John)

Logic programming

dengan syarat C1 adalah constant symbol yang baru, disebut Skolem

Resolution

constant

Ringkasan

Menghilangkan quantifier dan variable IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Menghilangkan ∀ Universal instantiation bisa digunakan berkali-kali untuk menambahkan kalimat baru. KB yang baru logically equivalent dengan yang lama. Menghilangkan ∃ Existential instantiation cukup digunakan sekali untuk menggantikan kalimat existential. KB yang baru tidak logically equivalent dengan yang lama, tetapi satisfiable jhj KB yang lama juga satisfiable → inferentially equivalent

Contoh IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

Andaikan KB berisi kalimat-kalimat berikut: ∀ x King(x) ∧ Greedy (x) ⇒ Evil(x) ∀ y Greedy (y ) King(John) Brother (Richard, John)


Jika kita mengambil semua kemungkinan instantiation dari kalimat universal, kita dapatkan KB sbb: King(John) ∧ Greedy (John) ⇒ Evil(John) King(Richard) ∧ Greedy (Richard) ⇒ Evil(Richard) Greedy (John) Greedy (Richard) King(John) Brother (Richard, John) KB yang baru dikatakan propositionalized: proposition symbol-nya: King(John), Greedy (John), Evil(John), King(Richard) etc.

Inference FOL menggunakan inference PL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Ide dasar: ubah KB + query dari FOL menjadi PL, lalu gunakan resolution.


Ide dasar: ubah KB + query dari FOL menjadi PL, lalu gunakan resolution. Masalah: dengan adanya function, jumlah ground term menjadi infinite Greedy (Father (John)) Greedy (Father (Father (John))) Greedy (Father (Father (Father (John)))), dst.


Ide dasar: ubah KB + query dari FOL menjadi PL, lalu gunakan resolution. Masalah: dengan adanya function, jumlah ground term menjadi infinite Greedy (Father (John)) Greedy (Father (Father (John))) Greedy (Father (Father (Father (John)))), dst. Teorema Herbrand (1930): jika FOL KB |= α, ada sebuah finite subset PL KB |= α. Ide dasar: For n = 0 to ∞ Buat propositional KBn dengan depth-n ground term Periksa apakah KBn |= α


Ide dasar: ubah KB + query dari FOL menjadi PL, lalu gunakan resolution. Masalah: dengan adanya function, jumlah ground term menjadi infinite Greedy (Father (John)) Greedy (Father (Father (John))) Greedy (Father (Father (Father (John)))), dst. Teorema Herbrand (1930): jika FOL KB |= α, ada sebuah finite subset PL KB |= α. Ide dasar: For n = 0 to ∞ Buat propositional KBn dengan depth-n ground term Periksa apakah KBn |= α Masalah (lagi!) kalau α di-entail OK, kalau tidak → infinite loop.


Ide dasar: ubah KB + query dari FOL menjadi PL, lalu gunakan resolution. Masalah: dengan adanya function, jumlah ground term menjadi infinite Greedy (Father (John)) Greedy (Father (Father (John))) Greedy (Father (Father (Father (John)))), dst. Teorema Herbrand (1930): jika FOL KB |= α, ada sebuah finite subset PL KB |= α. Ide dasar: For n = 0 to ∞ Buat propositional KBn dengan depth-n ground term Periksa apakah KBn |= α Masalah (lagi!) kalau α di-entail OK, kalau tidak → infinite loop. Teorema Church-Turing (1936): Entailment untuk FOL bersifat semidecidable.

Masalah dengan propositionalization IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Propositionalization menghasilkan banyak kalimat irelevan. Contohnya, dari KB berikut: ∀ x King(x) ∧ Greedy (x) ⇒ Evil(x) ∀ y Greedy (y ) King(John) Brother (Richard, John) manusia bisa cepat mengerti kalau Evil(John), namun propositionalization menghasilkan: King(Richard) ∧ Greedy (Richard) ⇒ Evil(Richard) Greedy (Richard) yang tidak relevan Dengan p buah predicate k -ary dan n constant, ada p × nk instantiation!


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Unification IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung

Isi KB

Mengubah FOL ke PL

∀ x King(x) ∧ Greedy (x) ⇒ Evil(x) ∀ y Greedy (y ) King(John) Brother (Richard, John)

Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming

Inference bahwa KB |= Evil(John) bisa langsung disimpulkan jika kita bisa mencari substitution θ sehingga King(x) dan Greedy (x) bisa “dicocokkan” dengan King(John) dan Greedy (y ). Contoh: θ = {x/John, y /John}

Resolution

Definisi unification

Ringkasan

U NIFY(α, β) = θ jika S UBST(α,θ) = S UBST(β,θ)

Contah unification IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

p Sayang(Anto, x)

q Sayang(Anto, Ani)

θ


p Sayang(Anto, x) Sayang(Anto, x)

q Sayang(Anto, Ani) Sayang(y , Ani)

θ {x/Ani}


p Sayang(Anto, x) Sayang(Anto, x) Sayang(Anto, x)

q Sayang(Anto, Ani) Sayang(y , Ani) Sayang(y , Ibu(y ))

θ {x/Ani} {x/Ani, y /Anto}


p Sayang(Anto, x) Sayang(Anto, x) Sayang(Anto, x) Sayang(Anto, x)

q Sayang(Anto, Ani) Sayang(y , Ani) Sayang(y , Ibu(y )) Sayang(x, Ani)

θ {x/Ani} {x/Ani, y /Anto} {y /Anto, x/Ibu(Anto)}


p Sayang(Anto, x) Sayang(Anto, x) Sayang(Anto, x) Sayang(Anto, x)

q Sayang(Anto, Ani) Sayang(y , Ani) Sayang(y , Ibu(y )) Sayang(x, Ani)

θ {x/Ani} {x/Ani, y /Anto} {y /Anto, x/Ibu(Anto)} fail

Standardized apart variable menghilangkan overlap, mis: Sayang(x101 , Ani) Lihat Figure 9.1 R&N2e untuk implementasi algoritma Unification


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Generalized Modus Ponens IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

Inference rule GMP p1 0 , p2 0 , . . . , pn 0 , (p1 ∧ p2 ∧ . . . ∧ pn ⇒ q) qθ di mana pi 0 θ = pi θ untuk semua i

Unification Inference Rule untuk FOL Forward chaining

p1 0 = King(John) p2 0 = Greedy (y ) θ = {x/John, y /John} qθ = Evil(John)

p1 = King(x) p2 = Greedy (x) q = Evil(x)

Backward chaining Logic programming Resolution Ringkasan

GMP dengan KB yang berisi definite clauses (seperti Horn clause pada PL): p1 ∧ p2 ∧ . . . ∧ pn ⇒ q Semua variable diasumsikan universally quantified GMP adalah hasil lifting MP: “mengangkat” inference rule PL ke FOL. Ada versi lifted untuk forward & backward chaining, resolution Kelebihan dibanding propositionalization: hanya melakukan substitution yang dibutuhkan oleh inference

Contoh knowledge base IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

Versi bahasa Inggris


“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 Col. West adalah criminal!

Penerjemahan Bhs Inggris ke FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

. . . it is a crime for an American to sell weapons to hostile nations:


. . . 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)


. . . 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:


. . . 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)


. . . 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 ) (Skolemization)


. . . 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 ) (Skolemization) . . . all of its missiles were sold to it by Colonel West


. . . 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 ) (Skolemization) . . . all of its missiles were sold to it by Colonel West Missile(x) ∧ Owns(Nono, x) ⇒ Sells(West, x, Nono)


. . . 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 ) (Skolemization) . . . all of its missiles were sold to it by Colonel West Missile(x) ∧ Owns(Nono, x) ⇒ Sells(West, x, Nono) Missiles are weapons:


. . . 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 ) (Skolemization) . . . 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)


. . . 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 ) (Skolemization) . . . 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”:


. . . 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 ) (Skolemization) . . . 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)


. . . 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 ) (Skolemization) . . . 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 . . .


. . . 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 ) (Skolemization) . . . 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)


. . . 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 ) (Skolemization) . . . 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 . . .


. . . 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 ) (Skolemization) . . . 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) Perhatikan: Semua kalimat KB ini berbentuk definite clause.


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Forward chaining pada FOL dengan GMP IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Mirip dengan forward chaining pada PL Mulai dari fakta yang diketahui (clause tanpa premise), mis: Owns(Nono, M1 ), Missile(M1 ) “Aktifkan” (trigger ) rule yang premise-nya diketahui (satisfied) → tambahkan kesimpulan rule ke KB, mis: Missile(x) ∧ Owns(Nono, x) ⇒ Sells(West, x, Nono) Ulangi sampai query terbukti, atau tidak ada fakta baru yang bisa ditambahkan ke KB. “Cocokkan” premise-premise setiap rule dengan fakta yang diketahui → pattern-matching dengan unification

Forward chaining pada FOL dengan GMP IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Algoritma forward chaining function FOL-FC-A SK(KB, α) returns a substitution or false repeat until new is empty new ← { } for each sentence r in KB do ( p1 ∧ . . . ∧ pn =⇒ q) ← S TANDARDIZE -A PART(r) for each θ such that (p1 ∧ . . . ∧ pn )θ = (p10 ∧ . . . ∧ pn0 )θ for some p10 , . . . , pn0 in KB q 0 ← S UBST(θ, q) if q 0 isn’t a renaming of sentence in KB or new then do add q 0 to new φ ← U NIFY(q 0 , α) if φ is not fail then return φ add new to KB return false

Contoh Forward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

American(West)

Missile(M1)

Owns(Nono,M1)

Enemy(Nono,America)

Contoh Forward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL

Weapon(M1)

Sells(West,M1,Nono)

Hostile(Nono)

Forward chaining Backward chaining Logic programming Resolution Ringkasan

American(West)

Missile(M1)

Owns(Nono,M1)

Enemy(Nono,America)

Contoh Forward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung

Criminal(West) Mengubah FOL ke PL Unification Inference Rule untuk FOL

Weapon(M1)

Sells(West,M1,Nono)

Hostile(Nono)

Forward chaining Backward chaining Logic programming Resolution Ringkasan

American(West)

Missile(M1)

Owns(Nono,M1)

Enemy(Nono,America)

Sifat Forward Chaining IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

Sound dan complete untuk first-order definite clause.

Unification

Datalog = first-order definite clause tanpa function. Time complexity FC pada Datalog → polynomial


Backward chaining

Tapi pada kasus umum, bisa infinite loop kalau α tidak di-entail. (Konsekuensi dari teorema Church-Turing: entailment adalah semidecidable)

Logic programming

Proses pattern matching pada premise NP-hard.

Forward chaining

Resolution Ringkasan

Pattern matching premise NP-hard? Diff(wa, nt) ∧ Diff(wa, sa)∧ Diff(nt, q) ∧ Diff(nt, sa)∧ Diff(q, nsw) ∧ Diff(q, sa)∧ Diff(nsw, v ) ∧ Diff(nsw, sa)∧ Diff(v , sa) ⇒ Colorable()

IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

NT Q


WA

Diff(Red, Blue) Diff(Red, Green) Diff(Green, Red) V Diff(Green, Blue) Diff(Blue, Red) T Diff(Blue, Green) Query A SK(KB,Colorable()) jhj CSP-nya menemui solusi! Terdapat kasus CSP 3SAT (satisfiability pada CNF dengan clause berukuran 3 literal) yang diketahui NP-hard. SA

NSW

Victoria


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Backward chaining pada FOL dengan GMP IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Algoritma backward chaining function FOL-BC-A SK(KB, goals, θ) returns a set of substitutions inputs: KB, a knowledge base goals, a list of conjuncts forming a query θ, the current substitution, initially the empty substitution { } local variables: ans, a set of substitutions, initially empty if goals is empty then return {θ} q 0 ← S UBST(θ, F IRST(goals)) for each r in KB where S TANDARDIZE -A PART(r) = ( p1 ∧ . . . ∧ pn ⇒ q) and θ0 ← U NIFY(q, q 0 ) succeeds ans ← FOL-BC-A SK(KB, [p1 , . . . , pn |R EST(goals)], C OMPOSE(θ0 , θ)) ∪ ans return ans

Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung

Criminal(West) Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan


Criminal(West)

{x/West}

Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

American(x)

Weapon(y)

Sells(x,y,z)

Hostile(z)


Criminal(West)

{x/West}

Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

American(West)

{}

Weapon(y)

Sells(x,y,z)

Hostile(z)


Criminal(West)

{x/West}

Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining

American(West)

Weapon(y)

{}


Missile(y)

Sells(x,y,z) Sells(West,M1,z)

Hostile(z) Hostile(Nono)


Criminal(West)

{x/West, y/M1}

Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining

American(West)

Weapon(y)

{}


Missile(y)

{ y/M1 }

Sells(x,y,z) Sells(West,M1,z)

Hostile(z) Hostile(Nono)


{x/West, y/M1, z/Nono}

Criminal(West) Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining

American(West)

Weapon(y)

Sells(West,M1,z)

{ z/Nono }

{}


Missile(y)

{ y/M1 }

Missile(M1)

Owns(Nono,M1)

Hostile(z)


{x/West, y/M1, z/Nono}

Criminal(West) Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining

American(West)

Weapon(y)

Hostile(Nono)

Sells(West,M1,z)

{ z/Nono }

{}


Missile(y)

Missile(M1)

Owns(Nono,M1)

Enemy(Nono,America)

{ y/M1 }

{}

{}

{}

Sifat Backward Chaining IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

Depth-first search: linear space complexity ^ ¨ incomplete (infinite loop) _ ¨ repeated state _ ¨

Prinsip dasar Logic Programming


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Apakah Logic Programming? IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung

Pemrograman dengan logika

Mengubah FOL ke PL

Program = deklarasi fakta yang bernilai true Execution = proses inference (backward chaining)


1. 2. 3. 4. 5. 6. 7.

Logic programming Identifikasi masalah Kumpulkan informasi Istirahat Repr. informasi dalam KB Repr. masalah sebagai query A SK(KB,query ) Cari fakta salah

Programming biasa Identifikasi masalah Kumpulkan informasi Pikirkan solusinya Tulis program (source code) Repr. masalah sebagai data Jalankan program terhadap data Debugging

(Harusnya) lebih mudah men-debug Ibukota(Bukittinggi, Indonesia) daripada x = x + 2 !

Prolog IKI30320 Kuliah 13 5 Nov 2007

Dasar: backward chaining pada Horn clause

Ruli Manurung

Banyak dipakai (EU,JAP “5th gen”)

Mengubah FOL ke PL

Program berupa himpunan clause: head :- literal1 , . . . literaln .


Contoh American(x) ∧ Weapon(y ) ∧ Sells(x, y , z) ∧ Hostile(z) ⇒ Criminal(x) criminal(X):-american(X),weapon(Y),sells(X,Y,Z),hostile(Z).

Aspek “non-logic” dari Prolog: BC berjalan atas-ke-bawah (rule) dan kiri-ke-kanan (clause) Ada predikat untuk aritmetika:: X is Y*Z+3 Ada clause dengan “efek samping”: I/O Closed-world assumption: “negation as failure”: hidup(X) :- not mati(X). hidup(anto) “benar” jika mati(anto) “salah”.

Contoh Prolog IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL

Implementasi DFS pada state X leluhur(X,Y) :- orangtua(X,Y). leluhur(X,Z) :- leluhur(X,Y),orangtua(Y,Z).


Meng-append dua list append([],Y,Y). append([X|L],Y,[X|Z]) :- append(L,Y,Z). query: append([1,2],[3,4],X) ? answers: X=[1,2,3,4] query: append(A,B,[1,2]) ? answers: A=[] B=[1,2] A=[1] B=[2] A=[1,2] B=[]


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Resolution pada FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung

Resolution inference rule pada FOL (lifting resolution PL): Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

`1 ∨ · · · ∨ `k , m1 ∨ · · · ∨ mn (`1 ∨ · · · ∨ ì−1 ∨ ì+1 ∨ · · · ∨ `k ∨ m1 ∨ · · · ∨ mj−1 ∨ mj+1 ∨ · · · ∨ mn )θ di mana U NIFY(ì , ¬mj ) = θ. Contoh: ¬Kaya(x) ∨ Sedih(x) Kaya(Anto) Sedih(Anto) di mana θ = {x/Anto} Gunakan resolution rule pada CNF (KB ∧ ¬α): complete untuk FOL

Mengubah FOL ke CNF IKI30320 Kuliah 13 5 Nov 2007

“Everyone who loves all animals is loved by someone:” ∀ x [∀ y Animal(y ) =⇒ Loves(x, y )] =⇒ [∃ y Loves(y , x)]

Ruli Manurung

1

Mengubah FOL ke PL

2

Unification Inference Rule untuk FOL Forward chaining Backward chaining

3

4

Logic programming Resolution

5

Ringkasan 6

Eliminasi implikasi dan biimplikasi ∀ x [¬∀ y ¬Animal(y ) ∨ Loves(x, y )] ∨ [∃ y Loves(y , x)] Pindahkan ¬ ke “dalam”: ¬∀ 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)] Standardize variables: setiap quantifier variable-nya beda ∀ x [∃ y Animal(y ) ∧ ¬Loves(x, y )] ∨ [∃ z Loves(z, x)] Skolemize: generalisasi existential instantiation. ∃ x diganti Skolem function universal quantified variable di “luar”: ∀ x [Animal(F (x)) ∧ ¬Loves(x, F (x))] ∨ Loves(G(x), x) Buang 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)]

Contoh pembuktian dengan resolution

L

L

L

L

Hostile(z)

Hostile(Nono)

Hostile(Nono)

L

L

L

L

L L

L

L

L

L

L

L

L

L L

L

L

L

L

L

L

L

Enemy(Nono,America)

>

Enemy(Nono,America)

Hostile(z)

Hostile(z)

>

Hostile(Nono)

Ringkasan

>

Hostile(x)

>

Enemy(x,America)

Owns(Nono,M1)

>

Owns(Nono,M1)

Owns(Nono,M1)

>

Logic programming

Missile(M1)

Sells(West,y,z)

Sells(West,M1,z)

>

Missile(M1)

Criminal(West)

Sells(West,y,z)

Sells(West,y,z)

>

Sells(West,x,Nono)

>

Owns(Nono,x)

Missile(y)

>

>

Missile(x)

Weapon(y)

>

Missile(M1)

Backward chaining

Resolution

Weapon(x)

Weapon(y)

>

Missile(x)


American(West)

>

Unification

Criminal(x)

>

American(West)

Mengubah FOL ke PL

Forward chaining

Hostile(z)

>

Sells(x,y,z)

>

Weapon(y)

>

American(x)

>

Ruli Manurung

L

IKI30320 Kuliah 13 5 Nov 2007

Hostile(z)


1

Mengubah FOL ke PL

2

Unification

3


4

Forward chaining

5

Backward chaining

Logic programming

6

Logic programming

Resolution

7

Resolution

8

Ringkasan


Ringkasan

Ringkasan IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan

60’an: Inference FOL melalui PL Unification Generalized Modus Ponens: FC + BC Logic programming: Prolog Resolution

IKI 30320: Sistem Cerdas Kuliah 13: Inference in FOL

Recommend Documents