Diskussion:Resolution (Logik)

Aber das ist doch Unfug. Selbst wenn ich, um das einfachste Beispiel zu nehmen, (A1 v A2) && (B1 v !A1) vergleiche mit A2 v B1, so erhalte ich für A1=0, A2=0, B1=1 sowie auch für A1=1, A2=1, B1=0 unterschiedliche Werte.

• Ist schon richtig so. Die Resolutions-Regel ist keine Äquivalenz, sondern (A1 v A2) && (B1 v !A1) impliziert nur A2 v B1. Für deine beiden Beispiele ist die Prämisse falsch und die Konklusion wahr, die Implikation also wahr. Starblue 18:51, 19. Apr 2004 (CEST)

• Die Resolutions-Regel bedeutet, daß die Erfüllbarkeit der Resolvente gegeben ist, wenn die zu resolvierenden Formeln erfüllbar sind. (A und B) erfüllbar => R(A,B) erfüllbar, mit R(A,B) Resolvente von A, B. Also im Umkehrschluss: Wenn R(A,B) nicht erfüllbar, so (A und B) nicht erfüllbar.

lineare Resolution

"jedem Resolutionsschritt immer mit der Resolvente des letzten Schritts"

Also ich hab das kennengelern als "SLD-Resolution" - ist aber auch egal wie man das nennt. Tatsache ist aber, dass diese Resolution IMHO nur für Hornformeln vollständig ist. Jedenfalls sagt das mein Prof.

SLD-Resolution ist eine spezielle Form der linearen Resolution. Die lineare Resolution ist vollständig, die SLD-Resolution hingegen nur für Hornformeln --guwac 03:06, 22. Jun 2005 (CEST)

Vielleicht könnte man auch noch die P-Resolution und die Input-Resolution nennen. Ich schau mal die Tage, ob ich was beitragen kann. -cljk 23:54, 9. Nov 2004 (CET)

Überarbeitung notwendig

"Resolution sollte im eigentlichen Sinne aber nur benutzt werden um die Unerfüllbarkeit einer Formel zu prüfen, da der Test auf Erfüllbarkeit nicht entscheidbar ist." Kompletter Bödsinn, wenn Unerfüllbarkeit entscheidbar ist, ist es Erfüllbarkeit auch. Der Gedanke hier ist, dass sowohl Erfüllbarkeit als auch Gültigkeit auf Unerfüllbarkeit zurückgeführt werden kann. Der komplette Artikel ist reichlich unstrukturiert, zusammengewürfelt, teilweise falsch und ungenau. Deshalb hab ich mal den Überarbeiten-Baustein gesetzt. --guwac 03:03, 22. Jun 2005 (CEST)

korrigiert --80.141.150.194 03:06, 29. Sep 2005 (CEST)

Ich war übrigens zu faul den Begriff der Klauselmenge einzubauen. Sollte man besser machen, sonst gibt's Ärger mitm Res-Operator ...--80.141.150.194 03:16, 29. Sep 2005 (CEST)

Aussagenlogische Resolution

Ich möchte die Verbesserung nicht selbst machen, dazu bin ich nicht versiert genug. Allgemein sollte aber auch folgendes im Kapitel enthalten sein:

• Allgemeine Resolution

(d.h. Sei gegeben (A1 und A2 und A3 und ...) folgt (B), dann Annahme das !(B) gilt, anschließender Widerspruchsbeweis um zu zeigen das die Konklusion stimmt/ nicht stimmt - hierfür kann DPP verwendet werden)

• die Davis-Putnam-Prozedur (DPP), ein Algorithmus zur Resolutionsführung für aussagenlogische Resolution

• Die Einheitsresolution für Horn-Klauseln

• Ein eigenes Kapitel für Horn-Klauseln

• Evtl. Graph- und Taubenschlag-Klauseln

Feinheiten abgeändert

Habe mal das '-F' durch '$\neg$F' ersetzt und das 'gültig' durch 'Tautologie'. Es fehlt aber noch einiges zur Resolution. Also, wer etwas fitter ist wie ich knn ja mal was dazu schrieben :-)

Ein logisches Rätsel

Ich behaupte mal, der Geführte Beweis ist falsch, weil die damit gefundene Lösung im Widerspruch zu den Aussagen 1 und 7 steht:

Wenn wie behauptet wird Platon Spartaner ist und Euklid Athener und damit kein Trottel(1), dann ist Diogenes Aussage: "Wenn Platon Spartaner ist, dann ist Euklid ein Trottel (7)..." falsch!

---

Ich gehe sogar noch n Schritt weiter und meine, dass das Rätsel keine Lösung hat: S(X) bedeutet "X ist Spartaner", A analog für Athener, ~ ist die Negation

Diogenes sagt "Wenn Platon Spartaner ist, dann ist Euklid ein Trottel (7)... ", ergo gilt:

1. S(P) - > ~A(E) -> S(E)

"...Die beiden kommen übrigens nicht aus derselben Stadt (8).", ergo gilt:

2. S(P) <-> ~S(E)

3. ~S(P) <-> S(E)

1. und 3. ergeben: S(P) -> ~S(P)

--217.235.96.250 14:21, 14. Jul. 2007 (CEST)

Hast Recht, Danke für den Hinweis. Habe das Beispiel vorerst zurück gezogen. Werde versuchen, es in den nächsten Tagen zu überarbeiten und wasserdicht zu machen. --Mussklprozz 14:55, 14. Jul. 2007 (CEST)

Getan. --Mussklprozz 10:08, 17. Jul. 2007 (CEST)

Beispiel Blumengießen

Das Beispiel Blumengießen passt nicht zum Artikel:

1. Es postuliert nur, dass sich per Resolutionskalkül ein Handlungsschema schlussfolgern lässt, ohne zu zeigen, wie dies geschieht. Der Satz Die Erarbeitung der logischen Klauseln, der Schlußfolgerungen und der Konsequenz sei dem Leser überlassen. ist eine Verhohnepipelung des Lesers.
2. Es führt den Begriff der Handlung und des Handlungsschemas ein, auf die im Artikel ansonsten kein Bezug genommen wird.

Ich lösche daher das Beispiel.

--Mussklprozz 18:18, 18. Jul. 2007 (CEST)

Verstoß gegen die guten Sitten

Hier hat Muss*pro* mindestens eine Urheberrechtsverletzung begangen.

An ihn: Du Brawnie gehst davon aus, dass die Nutzer Mathematiker und dumm sind. Dem ist nicht so. Es wäre auch unlogisch. Ein ästhetisches Beispiel ist immer besser als ein (ver-)klausuliertes, das sich nicht einmal mit einem Automaten nachrechnen laesst.

--82.83.113.233 19:37, 19. Jul. 2007 (CEST) --Jens611 19:42, 19. Jul. 2007 (CEST)

Nachtrag Name ist Schall und Rauch? Brawn = Muskeln [1] bzw. Brawnie = Muskelprotz.

Da scheinst du dir also auch im Englischen deine eigene Sprache gebastelt zu haben. Wenn, dann meinetwegen "beef cake" - aber auch das wäre ohne Relativierung durch Smilies oder wenigstens ein paar Anführungszeichen nur als Beleidigung zu werten. Also noch einmal: Lass das. Eine Beleidigung ist jedenfalls allemal ein Verstoß - nicht nur gegen die "guten Sitten"! --Reinhard Kraasch 20:43, 20. Jul. 2007 (CEST)

Resolvieren nach mehreren Literalen/Resolution erbringt keine leere Menge

Nehmen wir an, ich hätte folgende Klauseln: F={{A,!B}, {!A,B}}. Dann darf ich nach dem Artikel nur nach einem Literal resolvieren, nehmen wir mal !B. Dann erhalte ich: R={A,!A}.

So, dieses Ergebnis sagt mir nun: die Formel ist erfüllbar, da ja die leere Menge nicht resolviert werden konnte. Aber was fange ich mit dem Ergebnis an? Man könnte sagen die Belegungen A(A) = 1 und A(!A) = 1 liefern ein Modell, aber sie schließen sich doch auch aus!?

Ich quetsch mich mal rein mit der Antwort: Die Literale einer Klausel stehen in einer Oder-Beziehung zueinander. Also ist die Resolvente in diesem Fall eine Tautologie.

Was gibt also eine Resolution an, die nicht die leere Menge ergibt? --77.7.8.8 16:16, 15. Dez. 2007 (CET)

Siehe Einleitung des Artikels: Resolution ist ein Verfahren des Widerspruchsbeweises. Es zielt prinzipiell nur darauf ab, die leere Klausel zu erzeugen. Alle anderen Ergebnisse werden schlicht nicht ausgenutzt - auch wenn sie in einem anderen Sinn aussagekräftig sind.

Mir ist klar, dass das hier kein Hilfeforum ist, aber ich denke meine Frage ist berechtigt... --77.7.10.95 12:59, 18. Dez. 2007 (CET)

Ich hoffe, meine kurze Antwort hilft Dir weiter. Gruß --Mussklprozz 19:25, 18. Dez. 2007 (CET)

Danke, natürlich hilft mir das weiter! Deshalb wird das mit der nicht leeren Resolution auch in keinem der Bücher erwähnt, die ich durchgesehen habe. Wir hatten das nur mal in einer Vorlesung, dass mit Hilfe der Resolution eine gültige Belegung angegeben wurde (aber das ist ja scheinbar nicht die Absicht der Resolution). --77.7.10.95 20:09, 18. Dez. 2007 (CET)

Quantorensymbole

Hallo,

im Artikel werden die eher ungewöhnlichen (wenn auch nicht falschen) Symbole , $\bigvee _{x}$ und $\bigwedge _{x}$ verwendet. Ich würde vorschlagen durch die wesentlich gängigeren Symbole $\exists x$ und $\forall x$ zu ersetzen.

Schönen Gruß Andreas

M. E. eine reine Geschmacksfrage. Beide Schreibweisen sind durchaus gebräuchlich. Wenn Dir $\exists$ und $\forall$ besser gefallen, dann ersetz' halt die Symbole in dem Artikel. Ich werde deshalb nicht beleidigt sein.  ;-) Gruß --Mussklprozz 19:07, 8. Jan. 2008 (CET)

Laufzeit

Haken hat anscheinend 1985 eine exponentielle untere Schranke für die Länge von Resolutionsbeweisen gezeigt, siehe http://www.tcs.informatik.uni-muenchen.de/~jjohanns/projekt.html#ref15 und http://www.tcs.informatik.uni-muenchen.de/~jjohanns/projekt.html

Kennt sich da jemand genauer aus und/oder hat jemand was drüber gelesen?

Gruß Roland

404 bei Weblinks

Der Link zum Skript des Professors der Uni Hamburg führt ins leere. 91.45.201.236 23:28, 27. Apr. 2016 (CEST)

Das andere Vorlesungsskript ebenso [Vorlesungsskript von Bernhard Beckert, 2006, Universität Koblenz-Landau (PDF-Datei; 197 kB)].

Mehrwertige Funktionen

Was ist mit ein- und mehrwertigen Funktionen gemeint?

Mehrere Funktionwerte? Zu verschiedenen Argumenten? Oder gar zum gleichen Multifunktion?

Oder Ist der Funktionswert ein n-tupel?

==>Das angegebene Beispiel zeigt eine ein- und und eine zweistellige Funktion. Solltes also nicht ein- und mehrstellige Funktionen heißen? Das würde zumindest Sinn geben. Vgl. Prädikatenlogik erster Stufe --Ernsts (Diskussion) 05:41, 19. Feb. 2018 (CET)

Res-Operator wird nicht definiert

Ich kenne hier die richtige Antwort nicht, aber mir ist aufgefallen, dass der Res-Operator, so wie es gerade drinsteht, nicht definiert wird. Es können ja verschiedene Literale resolviert werden, also ist R nicht eindeutig bestimmt. Ich würde vermuten, dass eigentlich folgendes gemeint ist: Res^1(F) ist F vereinigt mit der Menge aller Resolventen, die aus F entstehen. Res^2(F) ist Res^1(Res^1(F)) usw... Res^*(F) ist dann soetwas wie der "Resolutionsabschluss" von F, das heißt die kleinste Menge von Klauseln, die F enthält und abgeschlossen unter Resolution ist. --Wandynsky (Diskussion) 22:03, 19. Feb. 2022 (CET)