Inferenzprozedur: Resolution

[Alexander]

Hallo,

ich habe mal eine Frage zur Resolution, und hoffe hier kann mir jemand
weiterhelfen:

Mittels Resolutionsprozedur kann bewiesen werden, ob eine Klausel F
aus einer Menge S von Klauseln hergeleitet werden kann. Dazu wird aus
der Vereinigung von S mit der negation von F ein wiederspruch
hergelietet.
Formal:
S |- F g.d.w. S & {!F} wiedersprüchlich g.d.w. S & {!F} |- {}
[1]

Was ist aber, wenn S schon in sich wiedersprüchlich ist?

z.B. soll bewiesen werden

in Mengendarstellung:
{A,!B},{!A},{!B},{B,C} |= {C}

bzw. in KNF
(A ODER NICHT B) UND (NICHT A) UND (NICHT B) UND (B ODER C) |= C

Aus den ersten drei Klauseln läßt sich eine leere Menge folgern.

Bedeutet das, aus einer Wiedersprüchlichen Menge kann alles abgeleitet
werden? Oder muss die zu beweisene Klausel unbedingt in die Resolution
miteinfließen? Oder darf eine derartige Menge überhaupt nicht für den
Beweis herangezogen werden?

Würde mich freuen, wenn das jemand kurz aufklären könnte.

Bis dann

Alexander

[1] Symbole:
Folgerungsoperator |-
Konjunktion (Vereinigung) &
Negation !