Not logged in. · Lost password · Register

IKnowNothing
Member since Feb 2018
3 posts
Subject: 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!
Jazzpirate
Member since Oct 2016
803 posts
Wurden bei der Musterlösung in dem Schritt "We skolemize:" die Variablen X W Z quasi durch sich selbst ersetzt?
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 :)

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?
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
IKnowNothing
Member since Feb 2018
3 posts
Alles klar, Verwirrung entwirrt - danke!
antiblond
Member since Oct 2013
40 posts
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?
tyr
Avatar
Member since Oct 2014
93 posts
Quote by antiblond:
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?
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
"Debugging is like doing surgery by randomly squeezing stuff in a patient's body and going like 'lmao tell me when this guy stops breathing'." -- Orteil, Creator of Cookie-Clicker
This post was edited 2 times, last on 2018-02-11, 13:22 by tyr.
antiblond
Member since Oct 2013
40 posts
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?
tyr
Avatar
Member since Oct 2014
93 posts
+1 Jazzpirate
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
"Debugging is like doing surgery by randomly squeezing stuff in a patient's body and going like 'lmao tell me when this guy stops breathing'." -- Orteil, Creator of Cookie-Clicker
This post was edited on 2018-02-11, 13:40 by tyr.
antiblond
Member since Oct 2013
40 posts
Ok, vielen Dank :)
Jazzpirate
Member since Oct 2016
803 posts
In reply to post #7
+1 tyr
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, *irgend*eine 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.
antiblond
Member since Oct 2013
40 posts
Jetzt hab ichs (glaube ich) tatsächlich verstanden. Dankeschön :)
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen