Die Unifikation ('Gleichmachung') von Termen spielt beim Beweisen mit Prolog eine zentrale Rolle. Zwei Terme sind unifizierbar, wenn sie identische atomare Terme sind oder sich in den Termen Variablen so substituieren lassen, dass die Terme Übereinstimmen. Komplexen Terme mÜssen dieselbe Stelligkeit aufweisen; ihre Argumente müssen paarweise unifizierbar sein. Die Substitution bindet eine Variable an einen Term. Der Term, in dem die Variable vorkam, wird durch die Substitution instantiiert.
Um eine Anfrage zu beweisen, sucht der Prolog-Interpreter in seiner Wissensbasis nach einer Klausel, die mit diesem Beweisziel unifiziert. Ist die Klausel eine Regel, so wird das Beweisziel durch den Regelrumpf ersetzt. Allfällige Variablen werden in jeder Klausel des Beweisziels jeweils an denselben Term gebunden. Nun wird die erste Klausel des Beweisziels gelöscht, um ein neues Beweisziel zu erhalten. Ist das Beweisziel leer, so ist der Beweis gelungen, wenn nicht, wird dieses Vorgehen wiederholt, bis das Beweisziel leer ist oder keine Unifikation mehr möglich ist (womit der Beweis misslungen wäre).
Stehen an einem Punkt mehrere Klauseln zur Unifikation zur Auswahl, setzt der Interpreter einen Entscheidungspunkt. Misslingt der Beweis, kehrt der Interpreter zum Entscheidungspunkt zurück und unifiziert mit der nächsten passenden Klausel. Dieses Verfahren heisst Backtracking.