Pengenalan
logika orde pertama
First order logic adalah sebuah bahasa formal
yang digunakan di ilmu matematika, philosophy, bahasa dan ilmu computer.
Disebut juga kalkulus predikat, merupakan logika yang digunakan untuk
merepresentasikan masalah yang tidak dapat direpresentasikan dengan menggunakan
proposisi. Logika predikat dapat memberikan representasi fakat-fakta sebagai
suatu pernyataan yang mapan (well form). Kalkulus predikat bisa menganalisakan
kalimat-kalimat ke dalam subjek dan argumen dalam berbagai cara yang
berbeda-beda, yang pada akhirnya kalkulus predikat bisa digunakan untuk
memecahkan problem of multiple generality (masalah dalam berbagai keadaan umum)
yang telah membingungkan sebagian besar ahli-ahli logika abad pertengahan.
Dengan menggunakan logika predikat ini, untuk pertama kalinya, para ahli-ahli
logika bisa memberikan quantifier yang cukup umum untuk merepresentasikan semua
argumen yang terdapat pada natural language.
Syntax
FOL: Elemen-elemen dasar
Elemen-elemen dasar FOL:
Constants : KingJohn, 2, UB, ITS, UI,
Malang, Depok , . . .
Predicates : Brother , >, Loves,
Membenci , Mengajar , . . .
Functions : Sqrt , LeftLegOf , Ayah, . . .
Variables : x , y , a, b, . . .
Connectives : ∧ ∨
¬ ⇒
⇔
Equality : =
Quantifiers : ∀ ∃
Semantics FOL : truth & model
Sama
halnya dengan. Proposisi Logic (PL), sebuah kalimat FOL bisa juga dikatakan
true terhadap sebuah model.
Namun,
sebuah kalimat bisa diinterpretasikan banyak cara dalam sebuah model.
Model
berisi :
Objects
: elemen-elemen di dalam dunia (domain elements).
Relations
: hubungan antara elemen-elemen tersebut.
Sebuah
interpretasi mendefinisikan referent (“yang dipetakan”)
Constant
symbols →
objects
Predicate
symbols →
relations
Function
symbols →
functional relations
Kemungkinan
model & interpretasi
Entailment , validity , satisfiability ,
dll. Didefinisikan untuk semua kemungkinan interpretasi dari semua kemungkinan
model!
Kalau mau dijabarkan semua kemungkinannya:
For each number of domain elements n from 1 to ∞ For each k -ary predicate Pk
in the vocabulary For each possible k -ary relation on n objects For each
constant symbol C in the vocabulary For each choice of referent for C from n
objects . . .
Menentukan entailment berdasarkan
truth-table? mustahil!
Biasanya ada satu interpretasi yang
“dimaksudkan” → intended interpretation.
Kamliat
Atom
Atomic sentence = predicate (term1,...,termn) or term1 = term2
Term = function (term1,...,termn) or
constant or variable
• Misal:
Brother(KingJohn,RichardTheLionheart) > (Length(LeftLegOf(Richard)),
Length(LeftLegOf(KingJohn)))
Kalimat
Komplek
• Kalimat komplek dibuat dari kalimat
atommenggunakan konektivitas S, S1 S2, S1 S2, S1 S2, S1 S2,
Misal: Sibling(KingJohn,Richard)
Sibling(Richard,KingJohn) >(1,2)
≤ (1,2) >(1,2)
>(1,2)
Universal
quantification
Syntax: Jika S kalimat, ∀ variables S adalah kalimat
Contoh:
“Semua mahasiswa PTIIK UB adalah Genius”
∀ x mahasiswa(x , PTIIKUB) ⇒ Genius (x)
Semantics: ∀ x S bernilai true dalam model m di bawah
interpretasi iff S bernilai true untuk semua kemungkinan referent dari x
(setiap object di dalam m). Dengan kata lain, ∀ x S ≡ conjunction dari semua instantiation S:
(mahasiswa(Ani , PTIIKUB) ⇒
Genius (Ani ))∧
(mahasiswa(Anto, PTIIKUB) ⇒
Genius (Anto))∧
.
. (mahasiswa(Zaenal , PTIIKUB) ⇒ Genius (Zaenal))∧
(mahasiswa(Zakky , PTIIKUB) ⇒ Genius (Zakky ))
Biasanya, ⇒ adalah operator /connective yang digunakan
dengan ∀.
Masalah yang sering terjadi : menggunakan ∧ sebagai connective untuk ∀ : ∀
x mahasiswa(x , PTIIKUB) ∧
Genius (x)
Kalimat ini berarti “Semua orang adalah
mahasiswa PTIIKUB dan Genius”.
Existential
quantification
Syntax : Jika S kalimat, ∃ variable S adalah kalimat
Contoh:
“Ada mahasiswa Gunadarma yang pintar”
∃ x mahasiswa(x , Gundarma ) ∧ pintar (x)
Semantics : ∃ x S bernilai true dalam model m di bawah
interpretasi iff S bernilai true untuk setidaknya 1 kemungkinan referent dari x
(sebuah object di dalam m). Dengan kata lain, ∃ x S ≡ disjunction dari semua instantiation S :
(mahasiswa(Ani , Gundar) ∧ pintar (Ani))∨
(mahasiswa(Anto, Gundar) ∧ pintar (Anto))∨
(mahasiswa(Zaenal , Gundar) ∧ pintar (Zaenal))∨
(mahasiswa(Zakky , Gundar) ∧ pintar (Zakky))
Biasanya, ∧ adalah operator /connective yang digunakan
dengan ∃.
Masalah yang sering terjadi : menggunakan ⇒ sebagai connective untuk ∃ : ∃
x mahasiswa(x , Gundar ) ⇒
pintar (x )
Kalimat ini true jika ada setidaknya 1
orang (object) yang tidak kuliah di Gunadarma!
Equality
Kalimat term1 = term2 bernilai true di
bawah sebuah interpretasi iff term1 and term2 me-refer ke object yang sama.
Contoh:
Ayah(Anto) = Abdul adalah satisfiable
Anto = Abdul juga satisfiable!
Anto = Anto adalah valid.
Bisa digunakan dengan negasi untuk
membedakan dua term: ∃
x , y Mencintai (Anto, x ) ∧
Mencintai(Anto, y ) ∧¬(x
= y ) (Anto mendua!)
Definisi Sibling: ∀ x , y Sibling(x , y ) ⇔ (¬(x
= y ) ∧ ∃ m, f ¬(m
= f ) ∧ Parent (m, x
) ∧ Parent (f ,
x ) ∧ Parent (m, y
) ∧ Parent (f ,
y ))
Mengubah
inferensi order pertama menjadi inferensi proposisi
Inferensi pada logika proposisi dapat
dilakukan dengan menggunakan resolusi. RESOLUSI adalah suatu aturan untuk
melakukan inferensi yg dapat berjalan secara efisien dalam suatu bentuk khusus
yg disebut Conjunctive Normal Form
(CNF).
•
CNF ini memiliki ciri-ciri sebagai berikut :
–
Setiap kalimat merupakan disjungsi literal
–
Semua kalimat terkonjungsi secara implisit
•
Dua atau lebih proposisi dapat digabungkan dengan menggunakan operator
logika :
a. Negasi : Ø (NOT)
b. Konjungsi : Ù (AND)
c. Disjungsi : Ú (OR)
d. Implikasi : ® (IF-THEN)
e. Ekuivalen : Û
• Operator NOT : digunakan untuk memberikan nilai negasi
(lawan) dari pernyataan yang telah ada.
Unifikasi
Unifikasi adalah usaha untuk mencoba
membuat dua ekspresi menjadi identik (mempersatukan keduanya) dengan mencari
substitusi-substitusi tertentu untuk mengikuti peubah-peubah dalam ekspresi
mereka tersebut. Unifikasi merupakan suatu prosedur sistematik untuk memperoleh
peubah-peubah instan dalam wffs. Ketika nilai kebenaran predikat adalah sebuah
fungsi dari nilai-nilai yang diasumsikan dengan argumen mereka, keinstanan
terkontrol dari nilai-nilai selanjutnya yang menyediakan cara memvalidasi
nilai-nilai kebenaran pernyataan yang berisi predikat. Unifikasi merupakan
dasar atas kebanyakan strategi inferensi dalam Kecerdasan Buatan. Sedangkan
dasar dari unifikasi adalah substitusi.
Rangkaian
Forward dan backward
Forward chaining merupakan metode inferensi
yang melakukan penalaran dari suatu masalah kepada solusinya. Jika klausa premis
sesuai dengan situasi (bernilai TRUE), maka proses akan menyatakan konklusi.
Forward chaining adalah data-driven karena inferensi dimulai dengan informasi
yang tersedia dan baru konklusi diperoleh. Jika suatu aplikasi menghasilkan
tree yang lebar dan tidak dalam, maka gunakan forward chaining.
Backward Chaining Menggunakan pendekatan
goal-driven, dimulai dari harapan apa yang akan terjadi (hipotesis) dan
kemudian mencari bukti yang mendukung (atau berlawanan) dengan harapan kita.
Sering hal ini memerlukan perumusan dan pengujian hipotesis sementara. Jika
suatu aplikasi menghasilkan tree yang sempit dan cukup dalam, maka gunakan
backward chaining.
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.
Sebelum resolusi dapat diterapkan, wff harus diletakkan dalam bentuk casual. Tujuan
dasar resolusi adalah membuat infer klausa baru yang disebut “revolvent” dari
dua klausa lain yang disebut parent clause.
Daftar Pustaka
http://otnaites.blogspot.co.id/2015/10/logika-first-order.html
http://slideplayer.info/slide/2919592/
https://www.google.co.id/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&cad=rja&uact=8&ved=0ahUKEwizu9vswvrWAhXLGpQKHT62A5AQFgguMAE&url=http%3A%2F%2Fshare.its.ac.id%2Fpluginfile.php%2F1370%2Fmod_resource%2Fcontent%2F1%2F9._First_Order_Logic.pdf&usg=AOvVaw3e59T03uvLJtbWfQymyxD7
http://denytrihartadi.blogspot.co.id/2017/01/inferensi-dalam-logika-order-pertama.html
http://afifrahma.blogspot.co.id/2013/01/resolusi-untuk-logika-predikat.html
Tidak ada komentar:
Posting Komentar