Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Mathematik » Logik, Mengen & Beweistechnik » Bedeutung des Resolutionskalküls
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule Bedeutung des Resolutionskalküls
semmelknoedel
Neu Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 12.07.2017
Mitteilungen: 2
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2017-07-12


Hallo Zusammen.

Ich arbeite gerade das Buch Logik für Informatiker von Uwe Schöning durch. Dort wird in Kapitel 1.1 die Wahrheitstafelmethode beschrieben, in Kapitel 1.4 das Resolutionskalkül.

Nun frage ich mich warum es das Resolutionskalkül überhaupt gibt, denn ich sehe gerade keine Vorteile gegenüber der Wahrheitstafelmethode.

- Das Resolutionskalkül benötigt bis zu <math>4^n</math> Schritte (laut Aufgabe 31) um die Unerfüllbarkeit zu zeigen.
- Die Wahrheitstafelmethode benötigt dagegen nur bis zu <math>2^n</math> Schritte (bzw. Zeilen) um die Erfüllbarkeit zu zeigen (und sogar eine konkrete Belegung zu liefern).

Wenn doch jetzt das Resolutionskalkül langsamer ist und das Ergebnis auch noch weniger Inhalt hat, warum hat es überlebt?

Gruß, Greg



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
lula
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 17.12.2007
Mitteilungen: 11131
Aus: Sankt Augustin NRW
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2017-07-12


Hallo
 das Resolutionskalkül kannst du einer Maschine überlassen, da es rein mechanisch ist.
Wie bringst du der Maschine bei eine Wahrheitstabelle zu erstellen?
bis dann, lula


-----------------
Mein Leben ist zwar recht teuer,  aber dafür bekomm ich jedes Jahr umsonst eine Reise einmal um die Sonne



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
dromedar
Senior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 26.10.2013
Mitteilungen: 5123
Aus: München
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, eingetragen 2017-07-12


2017-07-12 13:38 - lula in Beitrag No. 1 schreibt:
das Resolutionskalkül kannst du einer Maschine überlassen, da es rein mechanisch ist.
Wie bringst du der Maschine bei eine Wahrheitstabelle zu erstellen?

Wahrheitstabellen lassen sich noch einfacher automatisieren als der Resolutionskalkül.

2017-07-12 12:25 - semmelknoedel im Themenstart schreibt:
Nun frage ich mich warum es das Resolutionskalkül überhaupt gibt, denn ich sehe gerade keine Vorteile gegenüber der Wahrheitstafelmethode.

- Das Resolutionskalkül benötigt bis zu <math>4^n</math> Schritte (laut Aufgabe 31) um die Unerfüllbarkeit zu zeigen.
- Die Wahrheitstafelmethode benötigt dagegen nur bis zu <math>2^n</math> Schritte (bzw. Zeilen) um die Erfüllbarkeit zu zeigen [...]

Die Worst-case-Komplexität nicht das einzige Maß zur Beurteilung von Algorithmen. Etwas vereinfacht gesagt braucht die Wahrheitstabellenmethode "immer" <math>2^n</math> Schritte, während der Resolutionskalkül für "interessante" Probleme mit deutlich weniger auskommt und nur für "böswillig konstruierte" Probleme mehr benötigt (vgl. etwa hier, letzter Absatz auf Seite 95).

Die gleiche Situation tritt z.B. bei Sortierverfahren auf. Quicksort ist von seiner Worst-case-Komplexität miserabel, für praktische Anwendungen ist das aber nicht wesentlich.


P.S. Willkommen im Forum.



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
semmelknoedel
Neu Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 12.07.2017
Mitteilungen: 2
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, vom Themenstarter, eingetragen 2017-07-13


Danke für den Verweis zu Ben-Ari.



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
semmelknoedel hat die Antworten auf ihre/seine Frage gesehen.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2020 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]