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.
Problem 10.2 First Order Resolution
Wurden bei der Musterlösung in dem Schritt “We skolemize:” die Variablen X W Z quasi durch sich selbst ersetzt?
Und für Y dann nach der zweiten Regel durch fy(X) wobei dieses X nichts mit dem X zu tun hat was vorher schon da war? Dass die Namen an sich egal sind, ist mir bewusst - ich will nur sicher gehen, dass ich das richtig verstehe.
Danke schon mal!
Ein Algorithmus würde an der Stelle neue Variablennamen generieren, nur um nicht darauf testen zu müssen was sonst für variablen frei in der Formel vorkommen (und der Einheitlichkeit halber). De facto gibt es aber natürlich prinzipiell keinen Grund, nicht einfach die selben Variablennamen weiterzubenutzen, wenn die Variablen außerhalb des zu-ersetzenden Quantors nicht vorkommen. In dem Sinne wurden die Variablen durch sich selbst ersetzt, ja 
Versteh ich nicht wirklich was du damit meinst, sorry.
Aber falls das deiner Verwirrung hilft: Hätten wir oben X durch X’ ersetzt, würde jetzt Y durch fy(X’) ersetzt
Alles klar, Verwirrung entwirrt - danke!
Ich hätte auch noch eine Frage. Gibt es eine Regel oder ein “Best practice”, wann man die ersetzten Variablen als Kleinbuchstaben und wann als Großbuchstaben schreiben sollte? Wäre es im Beispiel also egal, ob ich [c/X] oder [C/X] mache?
Außerdem: Warum genau wurde Y durch f_Y(X) ersetzt und nicht einfach durch eine einzelne Variable? Existiert f() irgendwo oder erfinden wir das?
kleingeschrieben c: ist eine Konstante, somit eine nullstellige Funktion
EDIT sry hier warn Fehler großgeschrieben A oder B , etc: sind Aussagen ODER Terme, je nach Kontext, sind meist fett gedruckt
großgeschrieben X oder Y, etc: ist eine Variable
Das sind Konventionen, die Herr Kohlhase mehr oder minder ausdrücklich in seiner Vorlesung benutzt
Vielen Dank, so in etwa hatte ich es auch im Kopf. Dann frage ich mich jetzt: Ersetze ich dann, wenn ich ein \forall oder \exists loswerden will, die Variable durch eine andere Variable oder durch eine Konstante?
Hängt damit dann vielleicht auch das mit dem f_Y(X) zusammen?
Resolution:
forall X.A mit true gelabelt: neue Variable einführen, und statt X setzen. Hier kannst du zB X_0 einführen, oder wie Jazzpirate oben sagt, einfach X durch X ersetzen.
forall X. A mit false gelabelt: neue funktion fx einführen, und statt X setzen. fx muss von allen freien Variable in forall X. A abhängen, was oben in dem fall dafür sorgt, dass da fy(X) stehen muss. Es kann aber auch sein, dass forall X. A keine freien Variable hat, dann ist fx von nichts abhängig, also fx() und das ist eine Konstante, also kannst du auch c_x schreiben
exists: eigentlich gibt es keine Regeln, also exists in forall umwandeln mit exists X. A == \neg forall X. \neg A und dann siehe oben
1 „Gefällt mir“
Ok, vielen Dank 
Again, what tyr said
Falls ihr euch das im Kopf herleiten/begründen wollt: Mit “Forall” gebundene variablen gelten für alle terme, die kann ich also als freie variablen lassen und während der resolution beliebig durch terme substituieren (=unifikation). Mit “exists” gebundene variablen sagen mir nur, dass das für ein bestimmtes element gelten, die ersetz ich also a priori durch feste konstanten (“Angenommen es gäbe so ein Element c…” - resolution beweist ja unerfüllbarkeit, ist also eigentlich ein Widerspruchsbeweis!). Außer dass welches-element-jetzt-tatsächlich-die-formel-erfüllt ja von allen freien variablen abhängen darf, also ist es bei freien variablen keine konstante sondern eine funktion die von den freien variablen abhängen darf.
Beispiel:
\forall X \exists Y Y<X (in den natürlichen zahlen)
Die Formel soll für alle X gelten, also mach ich mit \exists Y Y<X’ (für eine potentiell neue variable X’) weiter. Jetzt weiß ich nur, irgendeine Zahl Y erfüllt das - welche hängt aber natürlich von dem jetzt freien X’ ab. also erfinde ich eine neue funktion f (“Angenommen es gäbe so ein Element f(X’)…” und mach daraus
f(X’)<X’. Jetzt darf ich resultion machen und für X’ beliebige Terme einsetzen und hätte z.B. für X’=0 den gewünschten Widerspruch.
1 „Gefällt mir“
Jetzt hab ichs (glaube ich) tatsächlich verstanden. Dankeschön