Hiho hab da mal ne Frage zur Resolventenbildung in Logik
(- = nicht)

Ich habe hier zwei Klauseln:
{ A , B , C , D } und { A, -B , C , D}

Wenn ich aus diesen beiden Klauseln nun einen Resolventen bilde ist das ja nicht weiter schwer...
das B fällt raus und die übrig gebliebenen Elemente vereinige ich.
Resolvent = {A , C , D}

Wenn ich nun aber zB die Klausenln
{ A , B , -C , D } & {A , -B , C , D }
habe, kann ich den beide Elemente in einem Schritt eleminieren ?
also Res: { A , D }?????

Oder muss ich irgend was anders machen ?

danke schön