ss2016 Resolutionsverfahren was macht man mit konstante?

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.

ss2016 Resolutionsverfahren was macht man mit konstante?
bei Resolutionsverfahren, bis jetzt eigentlich bei mir gut .
Aber jetzt komme ich verzwelfeln!
unter der pad gibt es eine Aufgabe von ss16,
c,d konstante, x,y,z variable,(unten)
eigentlich konstante darf nicht die funktionsvaribale einsetzen oder? warum mach der in unter stehende Aufagbe , in mgu1, c,d varibale trotedem eingestzten?
aufgabe :https://www.dropbox.com/s/vtnxeq9cyu5te6e/Braindumop.pdf?dl=0
loesung :https://www.dropbox.com/sh/7m36sbw902y4e8e/AABvQZhuevt2lf4LhZ-bHsDoa?dl=0&preview=PHOTO_20170330_131955.jpg


bei Resolutionsverfahren, bis jetzt eigentlich bei mir gut .
Aber jetzt komme ich verzwelfeln!
unter der pad gibt es eine Aufgabe von ss16,

[color=crimson]c,d konstante, x,y,z variable,(unten)
eigentlich konstante darf nicht die funktionsvaribale einsetzen oder? warum mach der in unter stehende Aufagbe , in mgu1, c,d varibale trotedem eingestzten?[/color]

aufgabe :https://www.dropbox.com/s/vtnxeq9cyu5te6e/Braindumop.…?dl=0
loesung :https://www.dropbox.com/sh/7m36sbw902y4e8e/AA…?dl=0&…


Konstanten darf man nicht ersetzten. In der Lösung wird auch keine Konstante ersetzt.

Variablen darf man beliebig ersetzten, egal durch was; auch durch Konstanten und andere Funktionssymbole. Deshalb ist die Substitution

x ↦ c
y ↦ d

auch erlaubt. Wenn etwas für alle x gilt, dann gilt es auch für die Konstante c. Andersherum dürfte man es natürlich nicht.


ah , ok, in der Loesung hat er variable eingesetzt nicht die konstante!! habe ich verlesen
bin wiederburuhigt.
danke