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
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
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)
Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
Contoh α = ∀ x mahasiswa(x, FasilkomUI) ⇒ pintar (x) β = ∃ x mahasiswa(x, Gundar ) ∧ pintar (x) σ = {x/Anto} S UBST(σ, α) menghasilkan instantiation:
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)
Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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:
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)
Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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)
Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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.
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. Masalah: dengan adanya function, jumlah ground term menjadi infinite Greedy (Father (John)) Greedy (Father (Father (John))) Greedy (Father (Father (Father (John)))), dst.
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. 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 |= α
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. 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.
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. 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!
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
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)
θ
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) Sayang(Anto, x)
q Sayang(Anto, Ani) Sayang(y , Ani)
θ {x/Ani}
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) Sayang(Anto, x) Sayang(Anto, x)
q Sayang(Anto, Ani) Sayang(y , Ani) Sayang(y , Ibu(y ))
θ {x/Ani} {x/Ani, y /Anto}
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) 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)}
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) 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
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
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
Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
“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:
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: American(x)∧Weapon(y )∧Sells(x, y , z)∧Hostile(z) ⇒ Criminal(x)
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: American(x)∧Weapon(y )∧Sells(x, y , z)∧Hostile(z) ⇒ Criminal(x) Nono . . . has some missiles:
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: American(x)∧Weapon(y )∧Sells(x, y , z)∧Hostile(z) ⇒ Criminal(x) Nono . . . has some missiles: ∃ x Owns(Nono, x) ∧ Missile(x)
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: 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)
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: 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
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: 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)
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: 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:
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: 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)
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: 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”:
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: 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)
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: 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 . . .
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: 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)
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: 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 . . .
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: 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.
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
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
Inference Rule untuk FOL
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
Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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
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
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
Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung
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)
Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung
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)
Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung
Criminal(West)
{x/West}
Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining
American(West)
Weapon(y)
{}
Backward chaining Logic programming Resolution Ringkasan
Missile(y)
Sells(x,y,z) Sells(West,M1,z)
Hostile(z) Hostile(Nono)
Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung
Criminal(West)
{x/West, y/M1}
Mengubah FOL ke PL Unification Inference Rule untuk FOL Forward chaining
American(West)
Weapon(y)
{}
Backward chaining Logic programming Resolution Ringkasan
Missile(y)
{ y/M1 }
Sells(x,y,z) Sells(West,M1,z)
Hostile(z) Hostile(Nono)
Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung
{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 }
{}
Backward chaining Logic programming Resolution Ringkasan
Missile(y)
{ y/M1 }
Missile(M1)
Owns(Nono,M1)
Hostile(z)
Contoh Backward Chaining FOL IKI30320 Kuliah 13 5 Nov 2007 Ruli Manurung
{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 }
{}
Backward chaining Logic programming Resolution Ringkasan
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
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
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)
Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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 .
Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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).
Unification Inference Rule untuk FOL Forward chaining Backward chaining Logic programming Resolution Ringkasan
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=[]
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
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 ∨ · · · ∨ `i−1 ∨ `i+1 ∨ · · · ∨ `k ∨ m1 ∨ · · · ∨ mj−1 ∨ mj+1 ∨ · · · ∨ mn )θ di mana U NIFY(`i , ¬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)
Inference Rule untuk FOL
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)
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
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