Entscheidungsproblem
Das Entscheidungsproblem ist die Frage, ob es einen Algorithmus gibt, der für einen beliebigen Ausdruck in der Prädikatenlogik bestimmt, ob es sich um eine Tautologie handelt oder nicht. Das Entscheidungsproblem wurde 1928 von David Hilbert gestellt und 1930 von Kurt Gödel negativ beantwortet (siehe Gödelscher Unvollständigkeitssatz). Zu den gleichen Ergebnis kamen 1936 Alan Turing und Alonzo Church, die das Problem von einer völlig anderen Perspektive beleuchteten (siehe Halteproblem).Allgemeiner bezeichnet man in der Theoretischen Informatik Probleme, für die zu einer gegebenen Eingabe als Lösung nur zwei Antworten (z. B. ja oder nein bzw. 0 oder 1 usw.) vorgesehen sind, als Entscheidungsproblem. Jedes solche Problem lässt sich als das Wortproblem einer formalen Sprache auffassen.
Eine formale Sprache S ist entscheidbar, wenn es eine berechenbare Funktion f gibt, sodass für alle Worte W über die Symbole der Sprache S gilt:
- f(W) = 1 genau dann wenn W in S liegt.
- f(W) = 0 genau dann wenn W nicht in S liegt.
- f°(W) = 1 genau dann wenn W in S liegt.
- f°(W) nicht definiert wenn W nicht in S liegt.