Modell

Ein sehr hilfreiches Werkzeug zum Beweis der Vollständigkeit der SLD-Resolution ist das Herbrand-Modell.

Es gilt nämlich: Eine Klauselmenge hat ein Modell genau dann wenn sie ein Herbrand-Modell hat. Man kann die Aussage sogar auf beliebige prädikatenlogische Formeln erweitern!

Somit kann man die Variablen in den Klauseln durch Konstanten aus dem Herbrand-Universum ersetzen und die Komplexität der Betrachtung enorm reduzieren.



(Das ist eine Erkenntnis aus dem Logischen Programmieren, einer Teildisziplin der Theoretischen Informatik. Bitte nicht runterbewerten, wenn du nichts damit anfangen kannst! Danke.)