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.
Unterschied RIF, RI2F und lRIF
Hallo zusammen,
ich hab mir mal die letzten Seiten im Skript durchgelesen und mir ist aufgefallen, dass es 3 verschiedene “Resolutionsmöglichkeiten” gibt (RIF, RI2F und lRIF). Bei RIF (vgl. S. 43) bildet man ja den MGU, um 2 Klauseln zu resolvieren. Laut Seite 47 ist lRIF die liberalisierte RIF, wobei es sich nicht um einen MGU, sondern einen beliebigen Unifikator handeln kann. Meine Frage zur lRIF wäre, was genau ist ein beliebiger Unifikator? Ist ein beliebiger, welcher nur einen Teil der 2 Klauseln unifiziert möglich?
Der RI2F ist laut S. 48 die Resolution with two-sided factoring. Irgendwie muss man da einen speziellen MGU bilden, was ich jetzt so ohne Beispiel nicht ganz verstehe. Wäre es möglich hierfür ein Beispiel zu bekommen?
Vielen Dank!
froschigon
Wenn du dir Lemma 51 anschaust, dann sind beliebige Unifikatoren einfach Spezialisierungen vom mgu, also eine Substitution die nach dem mgu angewendet wird.
Man hat zB die Klauselmenge {f(c)}, {¬f(x), ¬f(y), ¬f(z)}; wobei c eine Konstante ist, die man dann natürlich nicht substituieren kann. Normalerweise müsste man jetzt drei mal resolvieren bis der Algorithmus unerfüllbar sagt. Wenn man aber „geschickt“ substituiert, hier [c/x, c/y, c/z] reicht es einmal zu resolvieren. Es funktioniert aber nur wenn die Substitution Idempotent ist (hier: [c/x, c/y, c/z][c/x, c/y, c/z] = [c/x, c/y, c/z]).
Edit: So habs ich verstanden, nicht 100% sicher.