Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Resolution weniger allgemeinerer Unifikator als mgu
Hallo,
darf man bei der Resolution für die Anwendung der RIF-Regel bei Klauseln für die Prädikatenlogik erster Stufe einen weniger allgemeineren Unifikator als den mgu verwenden oder muss man den mgu verwenden?
Außerdem: Ist die etwas weiter im Skript vorne definierte Spezialisierungsregel auf eine allgemeine Substitution oder nur auf einen mgu definiert?
LG Gabriel
(lRIF) macht meines Wissens genau das, einen belibigen Unifikator verwenden. Das Lemma aus der Vorlesung besagt, dass jede mit (lRIF) herleitbare Formel auch mit (RIF) herleitbar ist.(Bzw. das Lemma selbst erwähnt glaube ich nur die Herleitung von {}. Im Beweis dazu hatten wird das aber glaube ich für beliebiges Hergeleitetes gezeigt.)