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.
First Order Resolution CNF Regeln
Im Skript wird auf Folie 455 bei der Elimination von ( \forall X . A )^T gefordert, dass Z \notin ( free(A) \union free(C) ). Würde es nicht ausreichen, an der Stelle Z \notin ( free(A) \ X \union free(C) ) bzw. Z \notin (free(\forall X . A) \union free(C) ) zu fordern?
Also nochmal in Worten: Sofern das durch den Allquantor gebundene X nur in A vorkommt, in den restlichen Klauseln aber nicht (frei), sollte ich das zuvor gebundene X doch durch ein nun freies X ersetzen können.
Joa, wenn Z=/=X ist das was du schreibst und in den Folien steht eh identisch.
Wenn Z=X würde deine Bedingung eher stimmen, aber nachdem wir unendlich viele variablen zur auswahl haben müssen wir uns um den Fall gar keine gedanken machen 
Genau um den Fall Z == X ging es mir ja auch, denn damit lässt sich eine Menge an sich unnötiges Umformulieren sparen. Insbesondere im Hinblick auf die Klausur kann man dann in mehreren Zeilen vorkommende gleiche Terme hinter Abkürzungen verstecken, wenn wir die Variablen darin ständig umbennen, ist das nicht mehr möglich. Außer wir verwenden Substitutionen auf unseren Termabbreviations, aber das verkompliziert dann eher als dass es hilft.
1 „Gefällt mir“