Frohe Weihnachten und einen guten rutsch im vorraus!
Hat jemand DIE GERINGSTE PLANNUG wie mann die zweite Aufgabe lösen kann?!?
http://www.informatik.uni-hamburg.de/WSV/f1/2002/Aufgaben/Blatt10.pdfIch hoffe das überhaupt jemand ins forum geht während der Ferien ;)
Hmm.. kann mich nicht daran erinnern, dass ich sowas mal gemacht habe [img]
http://www.sternenvolk.de/symb/24.gif[/img].
Versuch doch mal, eine Allgemeine Darstellung dieser Klauselmengen aufzuschreiben und anschließend, die verschiedenen Resolutionsverfahren anzuwenden. Vielleicht ist dann irgendetwas auffällig.
Ansonsten - schau in den Musteraufgaben und Lösungen der vergangenen Jahre nach, vielleicht wiederholt sich diese Aufgabe..(?)
..Oder du wartest, bis Slater vorbeischaut, der weiß das alles noch [img]
http://www.sternenvolk.de/symb/22.gif[/img]
..Oder du wartest, bis Slater vorbeischaut, der weiß das alles noch [img]http://www.sternenvolk.de/symb/22.gif[/img]
naja, was nicht dran war kann ich auch nicht erinnern..,
ansonsten klingt das ziemlich gestellt,
vielleicht hab ich irgendwann mal lust, zu versuchen dort einen sinn zu entdecken, aber 3 punkte.. [img]
http://www.sternenvolk.de/symb/22.gif[/img]
So, jetzt wo ich mich an's Studium gewoehnt habe, koennt ich ja vielleicht die Zeit finden, hier oefter mal vorbeizuschaun :)
Also, bei der zweiten Aufgabe bin ich mir auch nicht sehr sicher (vorallem bin ich mir nicht so ganz sicher, was sie soll, ich hab' sie als Uebung benutzt mir ueber die verschiedenen Resolutionsverfahren mal ein paar Gedanken zu machen - vielleicht war's ja auch so gedacht :) )
Gemacht hab' ich letztendlich folgendes: Zu jedem Resolutionsverfahren habe ich einen kleinen Text geschrieben, was sie in diesem Fall bringen und verucht mir zu ueberlegen wie effizent sie waren.
Es liegt ja eine Hornformel vor, die aus Klauseln besteht, die einen von drei Typen haben kann:
i) Klausel enthaelt negative Literale und ein positives Literal.
ii) Klausel enthaelt nur negative Literale
iii) Klausel enthaelt genau ein positives Literal.
Zuerst kann man sich ueberlegen, dass (per Vorgabe) nur eine Klausel des Typs ii) vorhanden ist, ferner kann das ganze nur zu unerfuellbar fuehren, wenn eine Klausel des Typs iii) vorhanden ist.
Bei der P-Resolution muss nun stets eine Klausel des Typs iii) beteiligt sein. Das reduziert die Anzahl der moeglichen Resolutionen erheblich. Ferner ist das Ziel klar: Aus Klauseln des Typs i) und iii) zuerst Klauseln so erzeugen, dass sie vom Typ iii) sind und all die Literale enthalten, die in F negiert vorkommen.
[F sei die gegebene Klausel, die nur negative Literale enthaelt]
Kann man das nicht machen, ist die Formel erfuellbar.
P-Resolution sollte insb. dann gut sein, wenn wenig Klauseln des Typs iii) auftreten.
Bei der N-Resolution muss immer die Formel F oder eine davon abgeleitete Formel bei der Resolventbildung auftreten, sonst waer's keine N-Resolution. Auch das reduziert die Anzahl der Moeglichkeiten erheblich.
Lineare Resolution: Da kann man das Sagen was im Skript steht (reduziert die Anzahl der Moeglichkeiten, fuehrt aber auch zu laengeren Ableitungen), ist hier imho nicht so schoen, da von der Wahl der Klausel abhaengt, von der man ausgeht. Daher hier der N- und P-Resolution unterlegen.
Stuetzmengenresolution: Enthaelt ja als Spezialfall die lineare Resolution und ist von der Wahl der Stuetzmenge abhaengig, daher hier auch nicht sinnvoll (Zuviele Moeglichkeiten, insbesondere, wenn die Hornformel gross ist).
Einheitsresolution: Aehnelt hier stark der P-Resolution mit selbigen Vorteilen.
Alle Verfahren sind (da wir mit einer Hornformel arbeiten) vollstaendig (und korrekt ohnehin), muessten also alle zum Ziel fuehren koennen. Am effektivsten sollte die P- oder N-Resolution sein.
Der Markierungsalgorithmus ist auch sehr gut (wahrscheinlich sogar noch besser), da die Formel bereits als Hornformel vorliegt (und umformen daher entfaellt) und es nur eine Formel gibt, bei die dazu fuehren koennte, dass unerfuellbar ausgegeben werden muss.
Zusammenfassung: Zuerst ueberpruefen, ob ueberhaupt unerfuellbar moeglich ist (d.h. Klauseln des Typs iii vorliegen), dann mit Markierungsalgorithmus oder P- bzw. N-Resolution dieses testen.
—
So ungefaehr hab' ich's gemacht, also mir zu jedem Verfahren ein wenig Gedanken gemacht.
Falls jemand eine bessere Idee hat immer raus damit :)
Cheers,
Frank
Mokrates, dein scheme proggi zur resolution funzt nich!
ich versuch die este aufgabe des 10 aufgaben blattes damit zu lösen und dein proggi findet die leere menge bei der ersten formel obwohl die formel sehr wohl gültig ist ( ich hab mir die mühe gemacht die wahrheitstafel zu machen )
(B \/ (¬A -> C)) /\ (A <-> C) /\ (B -> A)
KNF davon: (B \/ A \/ C) /\ (¬A \/ C) /\ (¬C \/ A) /\ (¬B \/ A)
falls du es selber ausprobieren willst ;)
Aba um ehrlich zu sein hab ich A raus und ich weiss der tafel zu folge das das auch nich stimmt. Falls jemand mir ma sagen kann was den richtige antwort iss wäre ich dieser person sehr verbunden ;P
hmm, bei der resolution kommt A als einzelne klausel raus, das bedeutet allerdings nicht, dass die formel zu A äquivalent ist (falls ich das mal bei meinen geschichten zur resolution behauptet habe, sorry [img]
http://www.fb18.de/gfx/9.gif[/img]),
das kann in spezialfällen so sein, allgemein bedeutet es aber logischerweise nur, dass die formel F und 'F /\ A' äquivalent sind,
was wiederum praktisch bedeutet, dass A immer wahr sein muss, damit F wahr ist, über die anderen atomaren formeln ist noch nix gesagt, F kann ja auch unerfüllbar sein,
vergleiche
{A,B} {-B} {-A} -> {A} -> LK, also unerfüllbar
@ slater mmmmh ok das habi gerallt.
aba das prog vom mokrates findet auf logische weise die leere menge raus, obwohl es eigentlich AUF KEINEN FALL sein kann:
{b c } aus {b a c } und {nicht a c }
{b a } aus {b a c } und {nicht c a }
{c nicht c } aus {nicht a c } und {nicht c a }
{c a } aus {b a c } und {nicht b a }
{c nicht b } aus {nicht a c } und {nicht b a }
{a } aus {nicht b a } und {b a }
{nicht a } aus {nicht a c } und {c nicht c }
{b } aus {b c } und {c nicht c }
{c } aus {nicht a c } und {c a }
{nicht b } aus {c nicht c } und {c nicht b }
{nicht c } aus {nicht c a } und {nicht a }
{} aus {a } und {nicht a }
tja was soll ich sagen [img]
http://www.fb18.de/gfx/10.gif[/img],
ich lads mir jetzt auch mal runter, aber ob ich scheme noch kann..
hast du denn die wahrheits tafel gemacht??
kriegst du da auch was erfüllbares raus??
vielleicht hab ich da schon den fehler gemacht?
oda sogar schon bei der umformung in KNF?
aba ich war mir so unsicher das ich alles doppelt und dreifach gemacht hab mit dem selben ergebnis…
aba wenn du zeit hast dann überprüf es trozdem lieber, auf mich ist nich immer verlass ;))
das kann man doch schnell nachprüfen, die zeile
{nicht b } aus {c nicht c } und {c nicht b }
aus dem programm ist doch falsch,
und resolution hab ich auf die schnelle auch mal erfolglos versucht
stiiiimmt, du hast echt gute augen! :)
ich hab auch nur A raus und die formel ist mit der formel /\ A äquivalent
aso müsste es das sein
thx :))
Hmmmm, kann mir jemand mal sagen, wie man die dritte Aufgabe aus Teil 1 Blatt 10 nun auf eine Tautologie prüft ? Vielen Dank schonmal.
Ich habs jetzt einfach mit gesundem Menschenverstand gemacht und argumentiert, dass die Formel für A(D)=0 z.B. falsch wird, also keine Tautologie sein kann. (Mag sein dass wir trotzdem die ellenlange Umformung machen sollen, aber dafür hab ich jetzt keinen Nerv)
Azure, zu deiner Argumentation, die Stützmengenresolution müsste doch bei Hornformeln als Stützmenge einfach alle Typ-3-klauseln enthalten, somit wäre sie, je weniger hiervon vorkommen, umso praktischer… oder nciht?
Tja, den Programmfehler sollte ich dann mal so schnell wie moeglich beheben, was? ,) Verdammter Mist. Naja, happens. Und ihr wart halt Alphatester… Aber wie gesagt, kann alles noch ein paar Tage auf sich warten lassen, da ich mir erst nochmal ein neues Netzgeraet anschaffen muss, da meines durchgebrannt ist. (Hofft mal fuer mich, dass mein Mainboard keinen Schaden genommen hat!)
MoKrates
XeXano, du hast dann nichts anderes als P-Resolution. Aber nichts hindert dich ja bei der Stuetzmengenresolution eine andere Stuetzmenge zu waehlen (so lange denn die Bedingungen erfuellt sind, also das F\T erfuellbar ist (F Klauselmenge, T Teilmenge) und bei jeder Resolution ist eine Klausel aus T beteiligt).
Bisschen unuebersichtlich der Thread :)
