Salah satu masalah dalam First Order Logic (FOL), adalah jika diberikan dua buah formula predikat, ingin diketahui apakah kedua formula tersebut dapat diunifikasi atau tidak. Jika kedua formula dapat diunifikasi, artinya kedua formula yang tampaknya berbeda secara sintaks, sesungguhnya sama satu sama lain. Tambahan lagi, jika kedua formula dapat diunifikasi, maka salah kedua formula dapati diubah menjadi bentuk yang sama secara sintaks melalui most general unifier (mgu).
Salah satu metode untuk memeriksa apakah sepasang formula predikat dapat diunifikasi adalah Algoritma Unifikasi Robinson (Robinson's Unification Algorithm). Algoritma unifikasi Robinson bekerja dengan membaca kedua formula dari kiri ke kanan sampai habis. Jika proses pembacaan menemukan disagreement set yang tidak dapat diunifikasi, maka kedua formula awal yang diberikan tidak dapat diunifikasi, atau dikatakan fail to unify. Jika proses pembacaan berhasil membaca kedua formula hingga selesai, maka artinya kedua formula awal yang diberikan dapat diunifikasi. Jika kedua formula dapat diunifikasi, maka algoritma unifikasi Robinson juga akan menghasilkan mgu.
Dalam setiap langkah mencari unifikasi dari kedua formula predikat, algoritma unifikasi Robinson membangun disagreement set, yang menampung simbol-simbol yang ditemukan berbeda dari kedua formula tersebut. Berikut ini diberikan dua buah contoh sederhana yang dapat digunakan untuk menggambarkan proses yang terjadi ketika algoritma unifikasi Robinson diterapkan. Sebelum membahas kedua contoh, perlu diketahui bahwa algoritma unifikasi ini diusulkan oleh John Alan Robinson pada tahun 1965.
Contoh 1
Diberikan dua formula predikat:\[A_{0}: p(a; x; f(g(y)))\] dan \[B_{0}: p(y; f(z); f(z))\]
Baca kedua formula tersebut mulai dari kiri ke kanan. Ketika membaca simbol predikat $p$, proses pembacaan tidak mengalami masalah, demikian juga ketika membaca tanda kurung buka. Perbedaan muncul
ketika pada formula pertama dibaca simbol konstanta $a$ sedangkan dari formula kedua dibaca simbol variabel $y$. Dari perbedaan ini dibentuk sebuah disagreement set
\[\{a, y\}\]
Dari disagreement set ini, bangun sebuah unifikator
\[\sigma_{1}: [y \leftarrow a]\]
Ketika sebuah unifikator dibentuk dari disagreement set, unifikator tersebut langsung diterapkan kepada kedua formula predikat. Jika unifikator $\sigma_{1}$ ini langsung diterapkan kepada kedua formula predikat, semua kemunculan variabel $y$ diganti dengan konstanta $a$, sehingga didapatkan sebuah pasangan formula predikat yang baru setelah dilakukan unifikasi:
\[A_{1}: p(a; x; f(g(a)))\] dan \[B_{1}: p(a; f(z); f(z))\]
Perhatikan bahwa variabel $y$ pada kedua formula diubah menjadi konstanta $a$.
Dari pasangan formula predikat yang baru didapatkan dalam iterasi kedua ini, proses pembacaan dilanjutkan. Proses pembacaan kedua formula predikat langsung mendapatkan sebuah disagreement set yang lain yaitu:
\[\{x, f(z)\}\]
Dari diasgreement set ini dibentuk sebuah unifikator baru:
\[\sigma_{2}: [x \leftarrow f(z)]\]
dan unifikator ini pun langsung diterapkan kepada kedua formula predikat dari iterasi ini sehingga didapatkan sebuah pasangan formula predikat ketiga:
\[A_{2}: p(a; f(z); f(g(a)))\] dan \[B_{2}: p(a; f(z); f(z))\]
Dalam iterasi berikutnya, proses pembacaan dilanjutkan kepada kedua formula predikat sehingga didapatkan sebuah disagreement set ketiga yaitu:
\[\{g(a), z\}\]
yang membentuk unifikator ketiga:
\[\sigma_{3}: [z \leftarrow g(a)]\]
untuk digunakan membentuk pasangan formula:
\[A_{3}: p(a; f(g(a)); f(g(a)))\] dan \[B_{3}: p(a; f(g(a)); f(g(a)))\]
Perhatikan bahwa variabel $z$ pada kedua formula juga ikut diubah.
Pada akhir iterasi ketiga ini didapatkan bahwa kedua formula tersebut ternyata serupa. Artinya, pasangan formula yang diberikan di awal dapat diunifikasi, dengan menggunakan mgu yang dibentuk dari unifikator $\sigma_{1}$, $\sigma_{2}$, dan $\sigma_{3}$:
\[\sigma = \sigma_{1} \sigma_{2} \sigma_{3} = [y \leftarrow a, x \leftarrow f(z), z \leftarrow g(a)]\]
Contoh 2
Diberikan dua formula predikat:
\[A_{0}: p(x; g(f(a)); f(x))\] dan \[B_{0}: p(f(y); z; y)\]
Seperti pada contoh sebelumnya, proses pembacaan diterapkan kepada kedua formula. Disagreement set pertama yang didapatkan adalah
\[\{x, f(y)\}\]
untuk membentuk unifikator:
\[\sigma_{1}: [x \leftarrow f(y)]\]
Pada iterasi kedua, proses pembacaan dilanjutkan kpeada pasangan formula yang baru:
\[A_{1}: p(f(y); g(f(a)); f(f(y)))\] dan \[B_{1}: p(f(y); z; y)\]
Disagreement set kedua adalah
\[\{g(f(a)), z\}\]
yang membentuk unifikator kedua:
\[\sigma_{2}: [z \leftarrow g(f(a))]\]
Unifikator ini digunakan untuk membentuk pasangan formula berikutnya:
\[A_{2}: p(f(y); g(f(a)); f(f(y)))\] dan \[B_{2}: p(f(y); g(f(a)); y)\]
Pasangan formula ini membentuk disagreement set
\[\{f(f(y)), y\}\]
Jika dibentuk sebuah unifikator, akan didapatkan
\[\sigma_{3}: [y \leftarrow f(f(y))]\]
Unifikator ini tidak dapat digunakan untuk me-unifikasi kedua formula yang diberikan, karena secara rekursif setiap kemunculan variabel $y$ akan berulang digantikan oleh simbol fungsi $f$. Artinya, pada contoh ini, unifikator $\sigma_{3}$ bukanlah unifikator, dan ini berarti bahwa pasangan formula awal yang diberikan tidak dapat diunifikasi.
Proses unifikasi pada contoh ini gagal, atau fail.
