RESOLUSI UNTUK LOGIKA PREDIKAT

SEJARAH RESOLUSI

Teknik resolusi diperkenalkan oleh J.A.Robinson pada tahun 1965.Teknik ini sebenarnya tidak dapat digunakan dengan mudah karena harus melalui beberapa tahap  dan setiap tahap tersebut memerlukan pengertian-pengertian dasar dari logika matemati Sebelum resolusi diterapkan, wff harus berada dalam keadaan normal (bentuk standar) yaitu hanya menggunakan V.

PENGERTIAN RESOLUSI

Resolusi merupakan kaidah inferensi utama dalam bahasa PROLOG.PROLOG menggunakan notasi “quantifier-free”.PROLOG didasarakan pada logika predikat urutan pertama.Sebelum resolusi diaplikasikan, wff harus berada dalam bentuk normal atau standard.

Tiga tipe utama bentuk normal :

1.         conjunctive normal form

2.         clausal form

3.         subset Horn clause.

            Dari pengertian dasar logika matematika tersebut,teknik resolusi tersusun secara bertahap sampai dengan proses resolve, yakni menghapus literal berpasangan yang asa pada setiap klausa untuk menghasilkan resolvent atau klausa hasil proses resolve. Dan dilakukan secara terus menerus sampai menghasilkan falsum.

Resolusi diaplikasikan ke dalam bentuk normal wff dengan menghubungkan seluruh elemen dan quantifier yang dieliminasi.

Contoh :

(A Ú B) Ù (~B ÚC)   ………… conjunctive normal form

Dimana  A Ú B  dan  ~B ÚC  adalah clause.

Logika proposional dapat ditulis dalam bentuk clause.Full clause form yang mengekspresikan formula logika predikat dapat ditulis dalam Kowalski clause form.

A₁, A₂, ……., A_N  à  B₁, B₂, ……., B_M 

Clause yang ditulis dalam notasi standard :

 A₁Ù A₂, ……., A_N  à  B₁ Ú B₂, ……., B_M 

RESOLUSI DAN LOGIKA PREDIKAT FIRT ORDER

Sebelum resolusi dapat diterapkan, wff harus diletakkan dalam bentuk casual

Contoh :

Some programmers hate all failures

No programmer hates any success

\ No failure is a success

P(x) = x is a progammer

F(x) = x is a failure

S(x) = x is a success

H(x,y) = x hates y

Premise dan kesimpulannya

(1)   ($x) [P(x) Ù ("y) (F(y) à H(x,y))]

(2)   ("x) (P(x) à ("y) (S(y) à ~H(x,y))]

(3)   ~("y) (F(y) à ~S(,y))

Konversi ke bentuk clausal :

1.      1. Hilangkan kondisional,   (p à q) º ~p v q

2.      Geser negasi ke dalam (reduksi skope ~). Negasi digeser hanya berlaku untuk atomik formula

3.      Hilangkan quantifier eksistensial

·         Jika $ tidak ada dalam skope ", ganti variabel dengan suatu konstanta baru ($x)   P(x)  diganti P(a)

·         Jika $ berada dalam skope ", ganti variabel dengan suatu fungsi yang memiliki argumen semua variabel dari " tersebut  "x ,"y , $z   P(x,y,z) diganti menjadi "x,"y, P(x,y,F(x,y))

4.      Standarisasi variabel (jika perlu) sehingga tiap quantifier memiliki variabel yang berbeda

5.      Geser semua " ke kiri (karena semua quantifier punya nama yang berbeda, pergeseran tidak mempengaruhi hasil) Bentuk ini disebut prenex normal form terdiri atas prefix quantifier yang diikuti matriks.Hilangkan "." tidak perlu ditulis, diasumsikan semua variabel terkuantifikasi universa.l Geser disjungsi (V) kedalam, sehingga terbentuk conjungsi normal formBuang konjungsi dan uraikan menjadi klausa-klausa

6.      Standarisasi variabel (jika perlu) sehingga tidak ada variabel yang muncul pada lebih dari 1 klausa.

Lakukan langkah-langkah resolusi pada CNF (BP Ù Øα), α adalah pernyataan yang harus dibuktikan Resolusi adalah teknik untuk membuktikan sebuah pernyataan pada logika proposional atau kalkulus predikat

            Refutasi=resolusi, membuktikan teorema dengan menegasikan pernyataan yang harus dibuktikan dan menambahkannya ke kumpulan aksioma yang diketahui benar

Semua aksioma dalam bentuk normal yaitu sebuah kalimat atau disjungsi beberapa kalimat

Pernyataan terbukti benar jika refutasi menghasilkan kalimat kosong

TUJUAN RESOLUSI     

Tujuan dasar resolusi adalah membuat infer klausa baru yang disebut “revolvent” dari dua klausa lain yang disebut parent clause.

Contoh :

                        A Ú B

                        A Ú ~B

                        \ A

Premis dapat ditulis :   (A Ú B) Ù (A Ú ~B)

Ingat Aksioma Distribusi :

            p Ú (q Ù r) º (p Ú q) Ù (p Ú q)

Sehingga premis di atas dapat ditulis :

(A Ú B) Ù (A Ú ~B) º A Ú (B Ù ~B) º A

 dimana B Ù ~B selalu bernilai salah

Tabel Klausa dan Resolvent

Parent Clause	Resolvent	Arti
p à q   , p atau ~p Ú q, p	q	Modus Pones
p à q , q à r atau ~p Ú q, ~ q Ú r	p à r atau ~p Ú r	Chaining atau Silogisme Hipotesis
~p Ú q, p Ú q	q	Penggabungan
~p Ú ~q,  p Ú q	~p Ú p atau ~q Ú q	TRUE (tautology)
~p, p	Nill	FALSE (kontradiksi)

SISTEM RESOLUSI DAN DEDUKSI

Refutation adalah pembuktian teorema dengan menunjukkan negasi atau pembuktian kontradiksi melalui reductio ad absurdum.

Melakukan refute berarti membuktikan kesalahan.

Contoh :

A à B

B à C

C à D

\A à D

Untuk membuktikan konklusi A à D  adalah suatu teorema melalui resolusi refutation, hal yang dilakukan :

p à q    º    ~p Ú q

sehingga 

Aà D    º    ~A Ú D

dan langkah terakhir adalah melakukan negasi

             ~(~A Ú D) º     A Ù ~D

Penggunaan konjungsi dari disjunctive form pada premis dan negasi pada konsklusi, memberikan conjuctive normal form yang cocok untuk resolusi refutation.

Dari contoh di atas, penulisannya menjadi :

(~A Ú B) Ù (~B Ú C) Ù (~C Ú D) Ù A Ù ~D

Akar bernilai nill, menunjukkan kontradiksi. Sehingga melalui refutation dapat ditunjukkan konklusi asli (awal) adalah teorema dengan peran kontradiksi.

RESOLUSI PADA PROPOSISI DAN PREDIKAT

1.Resolusi pada Logika Proposisi

Menggunakan resolusi yaitu suatu teknik pembuktian yang lebih efisien, sebab fakta-fakta yang akan dioperasikan terlebih dahulu dibawa ke bentuk standar yang sering disebut dengan nama klausa.Pembuktian suatu pernyataan menggunakan resolusi ini dilakukan dengan cara menegasikan pernyataan tersebut, kemudian dicari kontradiksinya dari pernyataan-pernyataan yang sudah ada.

Algoritma konversi ke bentuk klausa :

1.      Eliminir a → b menjadi ¬ a v b

2.      Reduksi skope dari ¬ sebagai berikut :

¬ (¬ a ^ b) ¬ a v ¬ b   

¬ (¬ a v b) ¬ a ^ ¬ b

¬ x : P(x) x : ¬ P(x)

¬ x : P(x) x : ¬ P(x)

2.Resolusi pada Logika Predikat

Logika predikat sebenarnya adalah logika proposional ditambah dengan hal-hal baru seperti kuantor, universe of discourse, term, predikat dan fungsi.

Resolusi pada logika predikat pada dasarnya sama dengan resolusi pada logika proposisi, hanya saja ditambah dengan unifikasi.Pada logika predikat, prosedur untuk membuktikan pernyataan P dengan beberapa pernyataan F yang telah diketahui, dengan menggunakan resolusi, dapat dilakukan melalui algoritma sebagai berikut :

1.      Konversikan semua proposisi F ke bentuk klausa

2.      Negasikan P, dan konversikan hasil negasi tersebut ke bentuk klausa.Tambahkan   kehimpunan klausa yang telah ada pada langkah

3.      Kerjakan hingga terjadi kontradiksi atau proses tidak mengalami kemajuan :

o   Seleksi 2 klausa sebagai klausa parent

o   Bandingkan (resolve) secara bersama-sama. Klausa hasil resolve tersebut  resolvent. Jika ada pasangan literal T dan ¬T2 sedemikian hingga keduanya dapat dilakukan unifikasi, maka salah satu T1 dan T2 disebut sebagai complementary literal. Jika ada lebih dari 1 complementary literal, maka hanya sepasang yang dapat meninggalkan resolvent

o   Jika resolvent berupa klausa kosong, maka ditemukan kontradiksi. Jika tidak, tambahkan ke himpunan klausa yang telah ada

•Diskusikan dengan memberikan contoh pembuktian dengan resolusi.

Contoh kasus :

Misalkan terdapat pernyataan-pernyataan sebagai berikut :

1.      Andi adalah seorang mahasiswa

2.      Andi masuk Jurusan Elektro

3.      Setiap mahasiswa elektro pasti mahasiswa teknik

4.      Kalkulus adalah matakuliah yang sulit

5.      Setiap mahasiswa teknik pasti akan suka kalkulus atau akan membencinya

6.      Setiap mahasiswa pasti akan suka terhadap suatu matakuliah

7.      Mahasiswa yang tidak pernah hadir pada kuliah matakuliah sulit, maka mereka pasti tidak suka terhadap matakuliah tersebut

8.      Andi tidak pernah hadir kuliah matakuliah kalkulus

Maka harus terlebih dahulu diubah ke dalam bentuk klausa sebagai berikut :

1.mahasiswa (Andi)

2.Elektro (Andi)

3.¬ Elektro (x1) v Teknik (v1)

4.sulit (Kalkulus)

5.¬ Teknik (x2) v suka (x2, Kalkulus) v benci (x2, Kalkulus)

6.suka (x3, f1 (x3))

7.¬ mahasiswa (x4) v ¬ sulit (y1) v hadir (x4, y1) v ¬ suka (x4, y1)

8.¬ hadir (Andi, Kalkulus)