Resolution in Prolog
Der Prolog-Interpreter versucht, Anfragen schrittweise durch Unifikation so weit zu substituieren, dass die leere Behauptung übrig bleibt (true)
- Alternative Entscheidungen (mehrere gültige Eingaben) erzeugen einen Lösungsbaum
- Baum wird nach Lösung durchsucht (SWI-Prolog: Tiefensuche)
- Bei Misserfolg (oder um weitere Lösung zu finden): Backtracking zur letzten Entscheidung
- Antwort „false“ möglich durch Closed-World-Assumption: „Negation by Failure“
SWI-Prolog (Bearbeitung der Anfrage):
- Auswahl des ersten Literals (links), dann schrittweise Auflösung nach rechts
- Bei Entscheidungen: Zuerst wird die erste (linke/obere) Möglichkeit versucht