Resolution

[die_nini]

Es geht um die Frage, was aus folgender Klauselmenge wird:
cl(!F) = {{ A, !B }{ !A, B }}

es ist ja eindeutig festgelegt, dass man immer nur 1 Literal entfernen darf, angenommen, ich entscheide mich für A/!A
dann ist meine resolvente {!B, B} und ich habe hier gewissermaßen einen tautologie, weil (!B v B) immer true ist. tautologien darf man ja wegstreichen? aber in diesem falle würde dann die leere klausel übrigbleiben?

deto gilt für B/!B!

hat irgendjemand einen besseren lösungsvorschlag?

[Christoph R.]

tautologien darf man ja wegstreichen? aber in diesem falle würde dann die leere klausel übrigbleiben?

Nein, wieso sollte die leere Klausel übrig bleiben? Je nachdem welches Atom man resolviert erhält man entweder {A, !A} oder {B, !B}. Beides sind Tautologien, die man streichen kann (und zwar die gesamte Klausel, nicht nur die enthaltenen Literale). Somit tritt man an der Stelle und wird nie die leere Klausel ableiten können. Das ist auch logisch, da die Klauselmenge offentlichtlich nicht unerfüllbar ist (setze z.B. A=true, B=true).

[hybrid]

Hab grad nachgeschaut, finde dazu nix, wo hast du das "eindeutig festgelegt, dass man immer nur 1 Literal entfernen darf" her? Aufgrund von Definition 3.60 kann mans schon so verstehn, aber zumindest seh ichs nirgends so explizit geschrieben.

[die_nini]

okay, damit wird einiges klarer.
das war ein denkfehler von mir. natürlich muss man alles wegstreichen und nicht nur den "inhalt" der klauseln.
danke jedenfalls :)

@hybrid: das hat er in der vorlesung mal erwähnt. und auf wikipedia und einigen anderen seiten ist das auch belegt!

[Christoph R.]

aber zumindest seh ichs nirgends so explizit geschrieben.

Ich glaube explizit steht es nirgends, aber Definition 3.60 sagt genau das aus. Es ist ja vom Literal A und nicht von einer Literalmenge die Rede.

Man darf jedenfalls in jedem Schritt immer nur ein Atom resolvieren (wenn man jetzt von der Robinson-Resolution in PL1 absieht - siehe 4.74). Das sieht man in obigem Beispiel auch, denn sonst könnte man ja dort (fälschlicherweise) die leere Klausel ableiten.

[die_nini]

aber eigentlich wird selbst bei definition 4.74 nur 1 literal entfernt, auch wenn eine menge von literalen dort steht...
man wählt ja einen unifikator, der aus den A1....Am klauseln eine klausel macht, zumindest hab ich das so verstanden.
wenn man nun hat
{{P(x, x), P(y, y) R(a, x)}, {!P(x, x), !P(y, y), R(a, v)}}
und man wählt den unifikator mgu{ x <- y}
dann mache ich im prinzip die beiden Prädikate P zu einem einzigen...und in folge entferne ich im endeffekt wieder nur 1 literal.

[Lynx]

Richtig, letzten Endes entfernt man nur ein Literal, auch wenn man durch vorherige Faktorisierung mehrere Literale einer Klausel zu einem einzigen zusammenfallen lässt. In der Robinson-Resolutionsregel wird das etwas abgekürzt gehandhabt, da ist dieser Vorgang nicht mehr so klar ersichtlich, aber im Prinzip ist es immer noch dasselbe.