oh grundsatzdiskussionen, die hab ich gerne,
vielen dank für das posting ;)
also entschuldigung aber etwas daran ist trotzdem noch "unlogisch".
Das heisst das es schon logisch ist (eine Klausel kann ja X mal vorkommen in der Formel aba nur ein mal ind der Klauselmenge) aba wenn wenn du jede klausel X mal benutzen kannst um zu reduzieren, dann gibt es doch so gut wie immer ein weg auf die leere menge zu kommen?!?
einen weg zur leeren menge zur kommen gibt es dann und nur GANAU DANN wenn die formel unerfüllbar ist,
vergleiche Resolutionssatz, bei mir:
"Eine Klauselmenge F ist genau dann unerfüllbar,
wenn LK (leere klausel) e Res*(F), d.h. F |-res LK."
und vergleiche Normalformtheorem:
"Für jede Formel F gibt es mindestens eine äquivalente Formel in KNF."
also das die LK rauskommt hat mit dem verfahren nix zu tun, das ist doch kein hokus pokus,
nimmst du eine formel wie
F = A und B, dann ist F wohl erfüllbar,
und das kannst du auch nicht durch resolution widerlegen,
die LK kann nicht resloviert werden, weil F eben nicht unerfüllbar ist
dagegen kommt man bei unerfüllbaren Formeln, wie die eine in der aufgabe, zur LK, da die formel unerfüllbar ist, auch wenn man das vielleicht nicht so deutlich erkennt vorher,
dafür ist ja der algorithmus dann da!
zu dem x-mal verwenden:
da muss man wider mit äquivanlenzen zaubern bzw. den algorithmus verstehen (also alles mal richtig durchlesen ;) )
begründung durch skript:
Resolventenlemma:
"Sei F eine Formel in Klauselmenge, …
mit R = (K1 - {L}) vereinigt (K2 - {-L}), [also R die Resolvente]
Dann sind F und (F vereinigt {R}) äquivalent."
also folgt, dass du genauso gut (F vereinigt {R}) auf unerfüllbarkeit prüfen kannst,
wenn du dort die LK findest, dann ist auch F unerfüllbar,
und in (F vereinigt {R}) hast du wieder alle ausgangsklauseln + die neue,
oder definition der Resolventenmengen:
da sieht man, das die resolventen auch im nächsten schritt dabeibleiben und nicht verschwinden
begründung durch formel:
ich nehm mal wieder mein beispiel von gestern:
2 klauseln {A,B,-D} und {A,B,D}
entspricht der formel F = (A OR B OR -D) AND (A OR B OR D),
dies ist nach adam riesling
== [ (A OR B) AND (A OR B OR D ] OR [ -D AND (A OR B OR D) ]
== (A OR B) OR [ (-D AND (A OR B)) OR (-D AND D) ]
== (A OR B) OR [ -D AND (A OR B) ]
== (A OR B)
da die beiden formeln F einerseits und (A OR B) andererseits äquivalent sind,
kannst du genausogut F AND (A OR B) schreiben, diese formel ist auch äquivalent zu den beiden vorherigen,
also schaust du jetzt in dieser dritten formel nach der LK,
die Formelmenge ist grad { {A,B,-D}, {A,B,D}, {A,B} },
die ursprünglichen klauseln sind hier also wieder dabei,
das kann man bei jeder resolventenbildung so machen,
es verschwinden also keine klauseln sondern es werden immer mehr, man darf sie sooft anwenden wie man will
noch ein beispielchen:
{{A,A,A,A,A,A},{-A}}
da kommt die leere klausel/ unerfüllbarkeit raus,
entweder durch resolution in vielen schritten:
{A,A,A,A,A,A},{-A} -> {A,A,A,A,A}
{A,A,A,A,A},{-A} -> {A,A,A,A}
{A,A,A,A},{-A} -> {A,A,A}
{A,A,A},{-A} -> {A,A}
{A,A},{-A} -> {A}
{A},{-A} -> LK
[edit]
ist wohl ein falsches beispiel, mengendarstellung mit doppelten kommt nicht so gut an..,
{{A},{-A}}
{A},{-A} -> LK
[/edit]
oder auf formelebene bisschen schneller ;):
(A OR A OR A OR A OR A OR A) AND -A
== A AND -A
== bottom
naja öfter mal durchlesen, gibt alles irgenwie sinn..
ausserdem habi grad was im skript gefunden ( bei mir 8 [ 9 ]), zitat:
{¬A,B} {¬A,C}
kein paar komplementäre literale!
keine Resolventenbildung!
wiederspricht das nich deine vorgehensart?!
das ist richtig das man da keine resolvente bilden kann,
einen zusammenhang zu meiner vorgehensart sehe ich allerdings noch nicht ;)
edit
dabei ist zu beachten, dass ich nicht
{B,D,A}, {A,D,B} Þ {A,D}
und dann spädda
{B,D,A}, {B,D} Þ {B,A}
geschrieben habe, sondern
{-B,D,A}, {A,D,B} Þ {A,D}
und später
{-B,D,A}, {-B,-D} Þ {-B,A}
