First Order Logic merupakan logika yang digunakan untuk memecahkan suatu rangkaian argumen, apakah rangkaian argumen tersebut berniali TRUE atau FALSE
Pada First Order Logic, terdapat object, relation, dan function :
- Object, yaitu hal-hal yang merupakan identitas suatu individu, seperti manusia, rumah, dan sebagainya
- Relation, yaitu hubungan antara benda yang satu dengan benda yang lainnya
- Function, yaitu suatu kondisi dari suatu object
Untuk mengerjakan First Order Logic, digunakan beberapa standar logic symbol seperti :
- connectives : ~(negative), Λ (conjunction), V(disjunction), →(implication)
- equality (=)
- quantifiers : ∀(for all), ∃(there exists)
Case Example :
- Marcus was a Man
- Marcus was a Pompeian
- All Pompeian were Roman
- Caesar was a ruler
- All Roman were either loyal to Caesar or hate him
- Everyone is loyal to someone
- People only try to assassinate rulers they aren’t loyal to
- Marcus tried to assassinate Caesar
- All men are People
Prove that Marcus is not loyal to Caesar
Untuk membuktikannya, pertama kita harus mengubah argumen-argumen tersebut ke dalam First Order Logic :
- Man(Marcus)
- Pompeian(Marcus)
- ∀x : Pompeian(x) → Roman(x)
- Ruler(Caesar)
- ∀x : Roman(x) → loyal(x, Caesar) V hate(x, Caesar)
- ∀x : ∃x : loyal(x,y)
- ∀x : ∃x : People(x) Λ Ruler(y) Λ assassinate(x,y) → ~loyal(x,y)
- assassinate(Marcus, Caesar)
- ∀x : Man(x) → People(x)
Setelah selesai mengubahnya menjadi First Order Logic, untuk membuktikan argumen tersebut dapat menggunakan 2 metode yaitu Backward Chaining dan Resolution. Pada setiap metode, kita harus menghubungkan suatu argumen dengan argumen lainnya hingga mendapatkan kondisi NULL
Backward Chaining
Resolution
Pada metode resolution, semua argumen tidak boleh memiliki hubungan implikasi sehingga harus diubah menjadi :
- Man(Marcus)
- Pompeian(Marcus)
- ~Pompeian(x) V Roman(x)
- Ruler(Caesar)
- ~Roman(x) V loyal(x, Caesar) V hate(x, Caesar)
- loyal(x,y)
- ~People(x) V ~Ruler(y) V ~assassinate(x,y) V ~loyal(x,y)
- assassinate(Marcus, Caesar)
- ~Man(x) V People(x)
Kemudian, untuk melakukan pembuktian dengan metode Resolution kita harus membuat negasi dari argumen yang ingin dibuktikan, kemudian kita pasangkan dengan argumen lain yang memiliki negasinya