hallo,
wir haben die zwei Klauseln K und K' udn die zwei Literale L1 und L2 (L1 != L2)
die in K vorkommen und deren Komplemente on K'. Nun sollen wir Begründen dass die Resolvenetenmethode nie mit K und K' resolvieren braucht.
Die Begründung habe ich bereits schon. Kann man bei hier K oder K' wegstreichen bzw. entfernen? Weil cih glaube nicht oder wie die resolviren erst also in den ersten schichten des baums ja mit K und ¬L1 und
K mit ¬L2 und erst in den späreteren schichten können die nicht mehr resolvieren. Aber eine resolootion braiucht ja immer eine Komplementmenge sonst funktioniert das ja nicht?
