Neue Antwort schreiben 
 
Themabewertung:
  • 0 Bewertung(en) - 0 im Durchschnitt
  • 1
  • 2
  • 3
  • 4
  • 5
Das Entscheidungsproblem? Kann das mal jemand erklären?
Der Doktor Offline
%0|%0

Beiträge: 7.872
Registriert seit: Dec 2008
Beitrag #1
Das Entscheidungsproblem? Kann das mal jemand erklären?
Mal wieder was für theoretische Informatiker:
Ich arbeite immernoch an meiner Facharbeit und muss kurz das Entscheidungsproblem und Entscheidbarkeit erkäutern. Leider steh ich dabei auf dem Schlauch!
Also Entscheidbarkeit habe ich verstanden, aber beim Entscheidungsproblem hänge ich. Ich habe schon an verschiedenen Stellen in Büchern gesucht und im Internet, aber ich komm' nicht so recht auf den Sinn.
Also ähm... Geht es doch eigentlich darum ob ein Algorithmus existiert der festellen kann ob ein Prädikat universell die Eigenschaft hat oder nicht in einem vorgegebenden System. Oder so ähnlich...
Kann mir das mal jemand kurz erklären oder mich auf eine vernüftige Seite verweisen?

Es ist besser nicht zu moderieren als falsch zu moderieren
(Dieser Beitrag wurde zuletzt bearbeitet: 12.02.2013 16:18 von Der Doktor.)
12.02.2013 16:12
Alle Beiträge dieses Benutzers finden Diese Nachricht in einer Antwort zitieren
gandro Online
Quälgeist

Beiträge: 8.950
Registriert seit: Jul 2008
Beitrag #2
RE: Das Entscheidungsproblem? Kann das mal jemand erklären?
Hab auch nur wenig Ahnung von der ganzen Geschichte, habe jetzt aber bisschen rumgeklickt (hauptsächlich englische Wikipedia und Math Stackexchange und das von mir schon erwähnte Logicomix), und versuche mich mal an einer Formulierung, ohne Garantie auf Richtigkeit.

Hier mal eine Formuilerung des Entscheidungsproblem (Quelle):
Entscheidungsproblem schrieb:Gibt es ein Verfahren, das für jede ausreichend formalisierte Aussage der Mathematik entscheidet, ob diese wahr oder falsch ist?

Das ist alles sehr unpräzise formuliert, was ist beispielsweise mit ausreichend formalisierte Aussage gemeint? Googlet man ein bisschen, dann steht praktisch überall dass sich das Entscheidungsproblem aus Aussagen in der "First-Order Logic" (FOL) (dt. Prädikatenlogik erster Stufe) bezieht.

Hier mal eine mathematische Aussage über Natürliche Zahlen: Für jede natürliche Zahl x existiert eine natürliche Zahl y die grösser ist als x.

Formuliert in First-Order Logic sieht das so aus (∀ steht "für alle" und ∃ für "es gibt"):
Zitat:∀ x ∃ y : y > x

Das ist eine mathematische Aussage, von der man jetzt beweisen könnte, dass sie wahr ist (in dem man beispielsweise zeigt, dass jeder Natürliche Zahl einen Nachfolger hat, die grösser ist als sie selber).

Es gibt auch noch "Second-Order Logic" oder "Prädikatenlogik zweiter Stufe" und andere Logiksysteme, die ich selber auch nicht wirklich kenne, in denen man aber Aussagen formulieren könnte.
Was für "First-Order Logic" beim Entscheidungsproblem jetzt wichtig scheint, ist der Vollständigkeitssatz von Gödel, der unter anderem besagt dass jede wahre Aussage in FOL auch beweisbar ist, was bei anderen Logiksystemen wohl nicht zwingend der Fall sein muss.

Um eine Aussage in FOL zu beweisen, benötigt man Axiome, also Aussagen die wir fix als wahr definieren, ohne sie beweisen zu müssen. Ein Beispiel für die Natürlichen Zahlen ist beispielsweise das Axiom: ∄ x : x + 1 = 0 ("es gibt keine natürlich Zahl, die mit Eins addiert wieder Null ergibt")

Kleiner Exkurs: Nicht alle Axiome der Natürlichen Zahlen lassen sich in FOL ausdrücken. Das heisst, dass das Entscheidungsproblem nicht mal für nicht alle mathematischen Aussagen eine Rolle spielt.

Des Weiteren kann der Informatiker "ein Verfahren" mit "einen Algorithmus" ersetzen, und und damit nur Programme meinen, die auch garantiert irgendwann mal terminieren, also in endlicher Zeit fertig werden mit Rechnen. Denke die Definition von Algorithmus ist dir eh schon klar, sonst kann ich das noch ausführen.

Das Entscheidungsproblem etwas mathematischer formuliert würde also lauten:
Entscheidungsproblem schrieb:Gibt es einen Algorithmus, der für jede mögliche Aussage in First-Order Logic (und optional zusätzlich einer endlicher Anzahl von Axiomen in First-Order Logic) entscheidet, ob die Aussage wahr oder falsch ist.

Die Antwort auf diese Frage lautet Nein. Es gibt keinen Algorithmus, der für jede mögliche mathematische Aussage entscheiden kann, ob sie wahr oder falsch ist. Das haben Church und Turing unabhängig 1936/37 gezeigt.

Das freut die Gewerkschaft der Mathematiker, denn das Finden und Beweisen von gültigen mathematischen Aussagen kann damit bewiesenermassen nicht durch Computer erledigt werden.

Turing hat beispielsweise gezeigt, dass wenn es einen Algorithmus gäbe, der für jede FOL-Aussage entscheidet, ob sie wahr oder falsch ist, dass man mit Hilfe davon auch das Halteproblem lösen könnte. Das Halteproblem kann aber nicht gelöst werden. Also kann es keinen Algorithmus fürs Entscheidungsproblem geben.


Paar Links die ich verwendet habe:
http://www.infomutt.com/e/en/entscheidungsproblem.html
http://www.infomutt.com/f/fi/first_order...culus.html
http://www.karlin.mff.cuni.cz/~stovicek/...bility.pdf
http://en.wikipedia.org/wiki/Entscheidungsproblem
http://www.cl.cam.ac.uk/teaching/0910/Co...ture-1.pdf
12.02.2013 18:48
Alle Beiträge dieses Benutzers finden Diese Nachricht in einer Antwort zitieren
Der Doktor Offline
%0|%0

Beiträge: 7.872
Registriert seit: Dec 2008
Beitrag #3
RE: Das Entscheidungsproblem? Kann das mal jemand erklären?
Danke,dass hat sehr geholfen und habs jetzt auch Verstanden. Das sind gute Quellen, komisch warum ich die in meiner mehrstündigen Rechere nicht gefunden habe. Vielleicht falsche Suchbegriffe...

Es ist besser nicht zu moderieren als falsch zu moderieren
12.02.2013 19:10
Alle Beiträge dieses Benutzers finden Diese Nachricht in einer Antwort zitieren
Neue Antwort schreiben 


Gehe zu:


Benutzer, die gerade dieses Thema anschauen: 1 Gast/Gäste