Vorschlag I
Prolog versucht eine Anfrage durch Unifikation zu beweisen, also jeweils zwei Terme durch das Ersetzen von Variablen (Substitution) gleich zu machen.
Dabei müssen alle Vorkommen einer Variablen in einem Term durch einen anderen Term ersetzt, bzw. an diesen gebunden werden. Der dadurch neu entstandene Term wird die Instanz des Ausgangsterms genannt.
Beim Beweisvorgang durchsucht Prolog die Wissensbasis von oben nach unten und setzt Entscheidungspunkte, wo es mehrere passende Klauseln für eine Variablenbindung gibt. Stellt sich die Entscheidung später als nicht beweisbar heraus, kehrt Prolog zurück, löst die letzte Variablenbindung und wählt stattdessen die nächstmögliche Klausel. Dieses Rückverfolgen wird Backtracking genannt.
Kommentar von Simon:
Vorschlag II
Beantwortet Prolog Anfragen, so beweist es, dass die resultierenden Antworten aus seiner Wissensbasis stammen.
Im Beweisprozess ist die Unifikation durch Substitution zentral. Hierbei werden zwei Terme durch punktuelles Ersetzen bestimmter Variablen identisch gemacht. Nicht jedes Termpaar ist jedoch unifizierbar; es gelten spezifische Rahmenbedingungen.
Muss Prolog eine Ergänzungs-Anfrage beweisen, so sucht es in seiner Wissensbasis ein passendes Faktum. Soll eine Ja/Nein-Anfrage bewiesen werden, sucht es nach einer passenden Regel. In einem zweiten Schritt werden spezifische Beweisregeln für Fakten bzw. Regeln angewendet. Gelangt man im Laufe des Prozesses in eine Sackgasse, ist Backtracking (Rückverfolgen) die Lösung.
Dieser gesamte Beweisprozess kann in einem Beweis-/Suchbaum visualisiert werden.
Kommentar von Simon: