Frage zum Resolutionskalkül

Benutzeravatar
igor.a
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 143
Registriert: 28. Sep 2009 16:05

Frage zum Resolutionskalkül

Beitrag von igor.a » 17. Jun 2010 08:02

Hallo,
teilweise erhält man bei diesem Verfahren Resolventen wie !q v q (z.B. aus den Klauseln !p v !q und p v q).
Soll man sie mit berücksichtigen oder weglassen, da ihr Wahrheitswert ja sowieso 1 ist und sie deshalb in einer Konjunktion nicht ausschlaggebend sind?

Benutzeravatar
olg
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 297
Registriert: 1. Okt 2008 19:24

Re: Frage zum Resolutionskalkül

Beitrag von olg » 17. Jun 2010 09:22

In der Vorlesung hatte Prof. Otto mal erwähnt, dass diese Klauseln überflüssig sind (da allgemeingültig) und daher auch nicht gebildet werden sollen, da ihr "Informationsgehalt" gleich 0 ist.

Gleiches war gestern in seinem Besuch der Übung der Fall, als es um "sinnlose Produktionen" wie {p,q},{p,r} auf {p,q,r} ging. Prinzipiell könnte man sie vielleicht ableiten (auch wenn nach der Regel eigentlich nur Literal und Komplement als Produktion verwendet werden darf), aber sie haben keinen nützlichen Inhalt.
"To Perl, or not to Perl, that is the kvetching." ~Larry Wall

kartzow
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 8. Apr 2010 14:12

Re: Frage zum Resolutionskalkül

Beitrag von kartzow » 17. Jun 2010 09:59

Bei deiner Frage hängt die Antwort natürlich etwas von der Aufgabenstellung ab:

Wenn du zeigen willst, dass eine Klauselmenge unerfüllbar ist, ist es natürlich richtig, dass du Klausen ohne Informationsgehalt nicht betrachten brauchst.

Wenn die Aufgabe dagegen ist, Res* zu berechnen, musst du natürlich alle Klauseln auch betrachten

Benutzeravatar
olg
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 297
Registriert: 1. Okt 2008 19:24

Re: Frage zum Resolutionskalkül

Beitrag von olg » 17. Jun 2010 18:10

kartzow hat geschrieben:Bei deiner Frage hängt die Antwort natürlich etwas von der Aufgabenstellung ab:

Wenn du zeigen willst, dass eine Klauselmenge unerfüllbar ist, ist es natürlich richtig, dass du Klausen ohne Informationsgehalt nicht betrachten brauchst.

Wenn die Aufgabe dagegen ist, Res* zu berechnen, musst du natürlich alle Klauseln auch betrachten
Die Aussage aus meinen Post stammt von Prof. Otto während der Aufgabe aus Übung 3, bei der es um Berechnung von Res* (für die Hornklauselmenge) ging. Entweder er hat sich dabei geirrt, oder es ist nicht nötig, diese für Res* zu bestimmen.
"To Perl, or not to Perl, that is the kvetching." ~Larry Wall

kartzow
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 8. Apr 2010 14:12

Re: Frage zum Resolutionskalkül

Beitrag von kartzow » 21. Jun 2010 08:13

Ok, um das klar zu machen, ein Beispiel.

Nehmen wir an wir an, wir starten mit den Klauseln

\(K= \left\{ \{p, q\} , \{\neg p , \neg q \} \{ q, r, s\} \right\}\)

dann sind \(\{ p, \neg p\}\) und \(\{q, \neg q\}\) natuerlich in \(Res^1(K)\)
und du musst sie bilden wenn du alle Elemente von \(Res^*(K)\) aufzaehlen willst.

In diesem Fall ist natuerlich auch klar, dass es keinen Sinn hat, zu versuchen aus einer dieser Klauseln eine neue zu erzeugen, denn wenn du \(\{ q, \neg q\}\) mit \(\{ q, r,s\}\) resolvierst, bekommst du natuerlich genau \(\{ q, r,s\}\) wieder raus. In dem Sinne musst du \(\{ q,\neg q\}\) nicht "weiterverarbeiten".

Das liegt aber nicht daran, dass diese Klausel immer den Wahrheitswert 1 hat, sondern an ihrer speziellen Struktur. Auch dazu ein Beispiel

\(K'=\left\{ \{ q, s\} , \{q, \neg q, r\} \right\}\)
Auch in diesem Fall ist der Wahrheitswert der zweiten Klausel immer 1, denn da steht ja quasi 1 oder r.
Trotzdem darf man diese Klausel nicht vernachlaessigen, wenn man \(Res^*(K')\) berechnen will:

Die Resolvente dieser beiden Klauseln ist die neue Klausel \(\{ q, r, s\}\) , die man nur bekommen kann, wenn man die immer wahre zweite Klausel mitbetrachtet. Also ist \(\{q,r,s\}\) in
\(Res^*(K')\), was man, wenn man die zweite Klausel nicht betrachtet, nicht herausfinden wird.

Fazit bis hierher: Fuer \(Res^*\) von einer Klauselmenge muss man auch immer wahre Klauselmengen betrachten, es sei denn sie sind genau von der Form \(\{q, \neg q\}\).


Wenn es hingegen nur um die Unerfuellbarkeit geht, kann man alle immer wahre Klauseln direkt aus der Betrachtung ausschliessen: Eine Klauselmenge K erweitert um immer wahre Klauseln K' ist unerfuellbar genau dann, wenn K schon unerfuellbar ist.

Ich hoffe, dieses ausfuehrliche Beispiel macht die Sache klar.

daniel_b
Computerversteher
Computerversteher
Beiträge: 363
Registriert: 15. Okt 2008 16:23

Re: Frage zum Resolutionskalkül

Beitrag von daniel_b » 7. Sep 2010 23:02

In den Musterlösungen werden Klauseln manchmal mehrfach zur Resolventenbildung benutzt. Kann ich eine Klausel mit beliebig vielen anderen Klauseln des selben Resolutionsschritts zusammenführen oder nur einmal für jedes Element dieser Klausel?

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Frage zum Resolutionskalkül

Beitrag von John » 7. Sep 2010 23:55

Beliebig oft. Semantisch werden Klauseln in einer Klauselmenge verundet, somit könntest du jede Klausel so oft duplizieren, wie du willst, denn es gilt \(\varphi \equiv \varphi \land \varphi\).
daniel_b hat geschrieben:In den Musterlösungen werden Klauseln manchmal mehrfach zur Resolventenbildung benutzt. Kann ich eine Klausel mit beliebig vielen anderen Klauseln des selben Resolutionsschritts zusammenführen oder nur einmal für jedes Element dieser Klausel?
DON'T PANIC

daniel_b
Computerversteher
Computerversteher
Beiträge: 363
Registriert: 15. Okt 2008 16:23

Re: Frage zum Resolutionskalkül

Beitrag von daniel_b » 8. Sep 2010 00:25

Okay, soweit stimmt das. Danke.

Ich hänge aber trotzdem an dem Problem, dass ich am Ende meiner Resolutionsschritte etwas wie {p, (nicht)p} stehen habe. Ist das äquivalent zur leeren Klausel zu betrachten? (Was wäre bei {p, (nicht)p, r} ?)

Anders formuliert: Was meinte kartzow oben damit, dass man solche immer wahren Klauseln "nicht weiter betrachten muss"?

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Frage zum Resolutionskalkül

Beitrag von John » 8. Sep 2010 01:01

Nein, die leere Klausel bedeutet, du hast "keine Alternative", sie ist also nicht wahr. \(\{p, \neg p\}\) ist zu interpretieren als \(p \lor \neg p\), was immer war ist. Da alle Klauseln semantisch verundet werden (und die einzelnen Literale in ihr verodert, siehe Definition Klausel u. Klauselmenge), kannst du \(\{p, \neg p\} \equiv \{\} \equiv 1\) aus der Klauselmenge also auch entfernen, ohne die logische Bedeutung der Klauselmenge zu verändern.
DON'T PANIC

daniel_b
Computerversteher
Computerversteher
Beiträge: 363
Registriert: 15. Okt 2008 16:23

Re: Frage zum Resolutionskalkül

Beitrag von daniel_b » 8. Sep 2010 02:55

Danke für deine Antwort, aber was sagt mir das jetzt? Ich lande jedes Mal, wenn ich (z.B. Übung 9-H1a ) durchgehe, bei solchen "immer wahren" Klauseln. Dann habe ich hinterher 3-4 Zweige auf dem Blatt, die alle in "immer wahr" enden, aber keine leere Klausel ergeben. (MuLö kommt recht schnell und ohne solche Probleme zur leeren Klausel.)

Ich meine mich zu erinnern, dass die Reihenfolge, in der ich die Klauseln verresolviere, völlig egal für das Ergebnis der Erfüllbarkeitsbestimmung ist. Mir ist daher nicht klar, wieso die Musterlösung direkt auf die leere Klausel kommt. Mach ich was falsch oder wurde in der MuLö einfach ein super-cleverer Trick benutzt, der die immer-wahren-Klauseln umgeht?

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Frage zum Resolutionskalkül

Beitrag von John » 8. Sep 2010 11:22

Naja, in der Musterlösung werden irrelevante Schritte nicht aufgeführt, sonst würde es in vielen Fällen schnell unübersichtlich werden. Sie ist ja nur eine Beispiellösung, und wenn du etwas Glück hast, erzeugst du auch nur Resolventen, die du benötigst, um die leere Klausel herzuleiten.
DON'T PANIC

daniel_b
Computerversteher
Computerversteher
Beiträge: 363
Registriert: 15. Okt 2008 16:23

Re: Frage zum Resolutionskalkül

Beitrag von daniel_b » 8. Sep 2010 12:27

Auch auf die Gefahr hin, dass es langsam nervt, aber wir kommen ja stetig näher... :mrgreen:

Ganz konkrete Frage, wo ich hänge:
Ich hab 8 Klauseln und verresolviere diese mal in Zweierpäckchen stur von links nach rechts, die Literale erlauben das im Beispiel. WAS mache ich, wenn ich dadurch in der nächsten Zeile dann vier "immer wahre" Klauseln erhalten habe?

Soll ich dann wie in Omas Rätselheft rumpuzzlen und wieder die ursprünglichen Klauseln dazunehmen, bis ich vielleicht (!) irgendwann mal auf die explizite leere Klausel komme? Hier weiß ich dank MuLö, dass es geht. Aber in der Klausur hätte ich damit dann ein "Halteproblem". :D

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Frage zum Resolutionskalkül

Beitrag von John » 8. Sep 2010 12:56

Wenn du eine Klausel der Form \(\{p, \neg p\}\) weiter verwendest, kommt dabei nie eine neue Klausel raus. Probiers doch mal ;) \(\{p, \neg p\} \cup \{p, q, r, ... \} = \{p, q, r, ...\}\). Und ein bereits vorhandenes Element in eine Menge einzufügen verändert die Menge bekanntlich nicht. Folglich sind solche Schritte unnötig. Ich denk mal, das beantwortet auch deine Frage über das Halteproblem, der Resolutionskalkül ist dementsprechend terminierend, da nur endlich viele neue Klauseln erzeugt werden können.
DON'T PANIC

daniel_b
Computerversteher
Computerversteher
Beiträge: 363
Registriert: 15. Okt 2008 16:23

Re: Frage zum Resolutionskalkül

Beitrag von daniel_b » 8. Sep 2010 18:30

Irgendwo reden wir aneinander vorbei.. :mrgreen:

Hier Meine 9/H1-a. Ergebnis müsste die leere Klausel sein.
Dateianhänge
reso2.jpg
reso2.jpg (55.63 KiB) 531 mal betrachtet

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: Frage zum Resolutionskalkül

Beitrag von John » 8. Sep 2010 18:48

Wichtig ist die Erkenntnis, dass du aus keiner wahren Klausel (wie die beiden markierten) jemals die leere Klausel herleiten kannst. Das geht nicht, denn aus etwas Wahrem kannst du keinen Widerspruch folgern. Solche Klauseln sind also ebenfalls unrelevant für das Bilden der leeren Klausel. Ich denk, das ist bei dir der springende Punkt. Wenn du mit einer Resolvente nicht die Unerfüllbarkeit zeigen kannst, ist das Bilden solcher zwecklos. Du brauchst (und solltest) sie also weder erzeugen noch weiterverwenden. Daher: Erzeuge mit dem Kalkül soviele "nicht trivialerweise wahre" Klauseln wie möglich, und wenn am Ende die leere Klausel drin steht, ists unerfüllbar, sonst erfüllbar.

Mit dem, was auf dem Zettel steht, bist du also noch nicht fertig, da weder alle (nicht trivialerweise wahre) Resolventen erzeugt wurden, noch die leere Klausel sich in der Menge befindet. In der ersten Iteration fehlen also noch Resolventen, mit der du die leere Klausel herleiten kannst.
DON'T PANIC

Antworten

Zurück zu „Archiv“