0 Daumen
9 Aufrufe

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?

vor von

Bitte logge dich ein oder registriere dich, um die Frage zu beantworten.

Ein anderes Problem?

Stell deine Frage

Willkommen bei der Stacklounge! Stell deine Frage sofort und kostenfrei

x
Made by a lovely community
...