Aufgabe:
Begründen Sie: Seien K und K′ Klauseln, so dass es zwei Literale L1 != L2 gibt, die in K vorkommen und deren Komplemente in K′ vorkommen. Dann braucht die Resolventenmethode nie K mit K′ resolvieren.
wenn L1 und L2 in K vorkommen und deren Komplemente in K' dann kann ich die ja nicht mit der Resolventenmethode resolvieren lassen, weil wenn ich mit der Resolventenmethode den Baum zeichne und K und K' resolvieren möchte habe ich ja entweder eine nutzlose Resolvente (also = true) oder keine Resolvente und wenn das der Fall ist kann ich dann K oder K' entfernen?
Kann ich dann K' entfernen, da in Ihr nur die Komplemente der Literale vorkommt?
Eine Aufklärung würde mir echt hefen. Vielen Dank!
LG