Algorithmus

Entscheidbarkeitsprobleme in der Logik

Informelle Charakterisierung:
• Theoreme zur Entscheidbarkeit / Unentscheidbarkeit semantischer Probleme • „Ein Algorithmus ist eine präzise, d.h. in einer festgelegten Sprache abgefasste,
endliche Beschreibung eines allgemeinen Verfahrens
• Aussagenlogik: unter Verwendung ausführbarer elementarer Verarbeitungsschritte.“
[Bauer & Goos, 1982; s.a. Folie 5 von P1]
Gültigkeit, Erfüllbarkeit, Unerfüllbarkeit, Folgerbarkeit, Äquivalenz sind entscheidbar
• Prädikatenlogik: Die intuitive Idee:
◊ Gültigkeit, Erfüllbarkeit, Unerfüllbarkeit, Folgerbarkeit, Äquivalenz • Ein Algorithmus legt fest, wie für ein vorgegebenes Problem (aus einer Klasse von
sind nicht entscheidbar Problemen) eine Lösung berechnet wird.
◊ Gültigkeit, Unerfüllbarkeit, Folgerbarkeit, Äquivalenz sind semi-entscheidbar • Alle Schritte der Problemlösung sind durch den Algorithmus festgelegt.
• Ausdruckskraft – Berechnungseigenschaften • Die Berechnung der Lösung ist nach einer endlichen Anzahl von Berechnungsschritten
abgeschlossen, d.h. der Algorithmus terminiert.
• Monadische Prädikatenlogik
• Aussagenlogik – Prädikatenlogik (eine Zusammenfassung) Die zentrale Frage:
• Das Dilemma: Ausdruckskraft – Berechnungseigenschaften • Wie kann die Idee des Algorithmus in einer präzisen, expliziten Weise charakterisiert
• Logik in der Informatik: Jenseits von F1 werden?
Î Theorie der Berechenbarkeit Î Vorlesung F3

Habel / Eschenbach Logik–13 [1] Habel / Eschenbach Logik–13 [2]

Theorie der Berechenbarkeit & Formalisierung des Begriffs des Problemklassen: Berechenbarkeit und Berechnungskomplexität
Algorithmus

Die Ausgangssituation: Gegeben ein Problem bzw. eine Problemklasse

• Gegeben ein Problem P. Gibt es einen Algorithmus, der P löst? • Gibt es Algorithmen, die das Problem lösen?
Prinzipiell zwei Möglichkeiten: D.h. existiert
• Es gibt einen Algorithmus, der P löst. Dies kann am besten dadurch gezeigt werden, • eine rekursive Funktion, die für das Problem als Eingabe einen Ausgabewert berechnet?
dass ein entsprechender Algorithmus angegeben und seine Korrektheit bewiesen wird. • eine Turing-Maschine, die für das Problem als Eingabe einen Ausgabewert berechnet?
• Es gibt keinen Algorithmus, der P löst. Dies kann nur dadurch gezeigt werden, dass
bewiesen wird, dass es keinen derartigen Algorithmus geben kann. Î Wenn ein derartiger Algorithmus existiert, heisst er berechenbar (computable).
• Konsequenz: Es muss eine explizite Definition des Begriffs ‘Algorithmus’ existieren, um Das Verfahren wird als effektiv bezeichnet.
überhaupt die Existenz eines Algorithmus’, der ein vorgegebenes Problem P löst, • Falls Algorithmen existieren, die das Problem effektiv lösen, dann stellt sich die Frage nach
untersuchen zu können. der Komplexität des Verfahrens.
Î Komplexitätstheorie: Komplexitätshierarchien
Die historische Entwicklung: Suche nach effizienten Verfahren.
• In den 20er- und 30er-Jahren: Suche nach Beweisverfahren in Logik und Mathematik.
• 1936 / 1937: Formale, explizite Definitionen von Berechenbarkeit und Algorithmus:
• Alonzo Church, Stephen Kleene, Emil Post: rekursive Funktionen • Fragen der Berechenbarkeit und Komplexität beziehen sich primär auf Problemklassen!
• Alan Turing: universal-algorithm machine Î Theorien der Berechenbarkeit und Komplexität Î Vorlesung F3

Habel / Eschenbach Logik–13 [3] Habel / Eschenbach Logik–13 [4]

 Probleme, Algorithmen, Entscheidungsprobleme Entscheidungsprobleme in Aussagen- und Prädikatenlogik

• Ein Problem P spezifiziert eine Funktion fP : DP → RP (‘Problemfunktion’). Entscheidungsprobleme:

DP spezifiziert die Probleminstanzen, RP die Lösungsinstanzen.
1. Gültigkeit einer Formel F bzw. einer endlichen Formelmenge {Fi | i ∈ Ι}
• Ein Algorithmus A spezifiziert / berechnet eine Funktion fA: DA → RA
(‘Algorithmusfunktion’). 2. Erfüllbarkeit einer Formel F bzw. einer endlichen Formelmenge {Fi | i ∈ Ι}
DA spezifiziert die Eingabeinstanzen, RA die Ausgabeinstanzen. 3. Unerfüllbarkeit einer Formel F bzw. einer endlichen Formelmenge {Fi | i ∈ Ι}

• Ein Problem P ist ein Entscheidungsproblem, 4. Folgerbarkeit einer Formel G aus einer endlichen Formelmenge {Fi | i ∈ Ι}
wenn fP eine Boolesche Funktion ist, d.h. wenn RP = {0, 1} bzw. RP = {false, true}. 5. Äquivalenz von zwei Formeln F und G bzw. zwei endlichen Formelmengen
• Ein Algorithmus A ist ein Entscheidungsalgorithmus, {Fi | i ∈ Ι} und {Gj | j ∈ J}
wenn fA eine Boolesche Funktion berechnet.
• Für jedes dieser Entscheidungsprobleme existiert eine aussagenlogische und eine
• Problem P ist entscheidbar, wenn die Boolesche Problemfunktion fP durch einen prädikatenlogische Variante:
Entscheidungsalgorithmus A berechnet wird, d.h. wenn fP = fA. • Für (1) – (3): DP = DA = LAL DP = DA = LPL
bzw. DP = DA = ℘(LAL) DP = DA = ℘(LPL)
• Für (4)): DP = DA = ℘(LAL) x LAL DP = DA = ℘(LPL) x LPL

Habel / Eschenbach Logik–13 [5] Habel / Eschenbach Logik–13 [6]

Entscheidbarkeitsresultate für die Aussagenlogik Unentscheidbarkeitsresultate für die Prädikatenlogik

• Gültigkeit einer Formel F bzw. einer endlichen Formelmenge {Fi | i ∈ Ι} Die Resultate:
• Erfüllbarkeit einer Formel F bzw. einer endlichen Formelmenge {Fi | i ∈ Ι} • Das Erfüllbarkeitsproblem ist in der Prädikatenlogik nicht entscheidbar.
• Unerfüllbarkeit einer Formel F bzw. einer endlichen Formelmenge {Fi | i ∈ Ι} • Das Gültigkeitsproblem ist in der Prädikatenlogik nicht entscheidbar.
Î Das Unerfüllbarkeitsproblem, das Folgerbarkeitsproblem und das Äquivalenzproblem sind
• Folgerbarkeit eine Formel G aus einer endlichen Formelmenge {Fi | i ∈ Ι} ebenfalls unentscheidbar.
• Äquivalenz von zwei Formeln F und G bzw. zwei endlichen Formelmengen
{Fi | i ∈ Ι } und {Gj | j ∈ J }
• Es gibt keinen Algorithmus, der bei Eingabe einer beliebigen prädikatenlogischen Formel
sind (für die Aussagenlogik) entscheidbar, denn: entscheidet, ob diese Formel erfüllbar ist.
• Wahrheitstafelmethode ist ein algorithmisches Verfahren, um Erfüllbarkeit bzw. • Es gibt keinen Algorithmus, der bei Eingabe einer beliebigen prädikatenlogischen Formel
Unerfüllbarkeit, und somit auch Gültigkeit und Folgerbarkeit, zu prüfen. entscheidet, ob diese Formel gültig ist.
• Der Resolutionsalgorithmus der Aussagenlogik entscheidet ebenfalls Erfüllbarkeit bzw.
Unerfüllbarkeit einer Formel (in KNF).
• Die Verfahren zur Prüfung von Formeln (auf Erfüllbarkeit bzw. Unerfüllbarkeit) können
auch zur Prüfung der entsprechenden Eigenschaften von Formelmengen verwendet werden.

Habel / Eschenbach Logik–13 [7] Habel / Eschenbach Logik–13 [8]

 Wie lässt sich Unentscheidbarkeit beweisen? Entscheidbarkeit / Semi-Entscheidbarkeit
Zwei „Klassiker“ der Unentscheidbarkeit:
• das Postsche Korrespondenzproblem Entscheidbarkeit eines Problems P
JA!
• das Halte-Problem für Turingmaschinen I hat die Eigenschaft P.
Î Beide Probleme sind unentscheidbar! Algorithmischer Test
Instanz auf die problemspezifische
Reduktionsmethode: Eigenschaft P
NEIN!
• Gegeben ein Problem P und ein bekanntermassen unentscheidbares Problem P*.
I hat die Eigenschaft P nicht.
• Reduktion von P auf P*, etwa in der folgenden Weise:
Bestimme ein Lösungsverfahren für P* auf der Basis eines – angenommenen –
Lösungsverfahrens für P. D.h.: zeige: Semi-Entscheidbarkeit eines Problems P
# Wenn P entscheidbar ist, dann ist P* entscheidbar. „Hat die Eigenschaft P!“ falls
• Also: Wenn die Beziehung # nachgewiesen ist, dann kann P nicht entscheidbar sein. I die Eigenschaft P hat.
Algorithmischer Test
Î Schönings Unentscheidbarkeitsbeweis (S. 72ff.) basiert auf einer Reduktion auf das Instanz auf die problemspezifische
Postsche Korrespondenzproblem. Eigenschaft P
Hält (eventuell) nicht an, falls
I die Eigenschaft P nicht hat.
Habel / Eschenbach Logik–13 [9] Habel / Eschenbach Logik–13 [10]

Semi-Entscheidbarkeitsresultate für die Prädikatenlogik Nicht-Semi-Entscheidbarkeit der Erfüllbarkeit in der Prädikatenlogik

• Das Erfüllbarkeitsproblem der Prädikatenlogik ist nicht semi-entscheidbar.

• Das Unerfüllbarkeitsproblem der Prädikatenlogik ist semi-entscheidbar.
Begründung: Resolutionsverfahren. Begründung:
• Das Gültigkeitsproblem der Prädikatenlogik ist semi-entscheidbar. • Wäre das Erfüllbarkeitsproblem semi-entscheidbar,
Begründung: Reduktion der Gültigkeitsprüfung auf Unerfüllbarkeitsprüfung so könnten wir folgenden Algorithmus konstruieren:
• Das Folgerbarkeitsproblem der Prädikatenlogik ist semi-entscheidbar.
Begründung: Reduktion der Folgerbarkeitsprüfung auf Unerfüllbarkeitsprüfung. Gegeben sei eine Formel F: Auf F wenden wir gleichzeitig die Semi-Entscheidungs-
algorithmen Au für Unerfüllbarkeit und Ae für Erfüllbarkeit an.

Î Jede gültige Inferenz kann als gültig nachgewiesen werden! Da F entweder erfüllbar oder unerfüllbar ist, würde entweder Au oder Ae nach endlich
vielen Schritten mit einem positiven Resultat terminieren.

Somit hätten wir ein Entscheidungsverfahren für Erfüllbarkeit und für Unerfüllbarkeit
konstruiert.

Î Es ist nicht möglich, alle nicht-gültigen Inferenzen als nicht-gültig nachzuweisen.

Habel / Eschenbach Logik–13 [11] Habel / Eschenbach Logik–13 [12]

 Monadische Prädikatenlogik Logiken: Ausdruckskraft und Berechnungseigenschaften

Monadische Formel (Definition)

Eine Formel F aus LPL ist monadisch, falls sie ausser den logischen Symbolen
Ausdruckskraft Berechnungseigenschaften
(Junktoren und Quantoren) sowie den Variablen und Konstantensymbolen Aussagenlogik keine interne Strukturierung • Entscheidbarkeit der
atomarer Aussagen Unerfüllbarkeit / Gültigkeit
nur einstellige Prädikatensymbole enthält.
Î nur ja/nein Fragen behandelbar • Erfüllbare Formeln haben
Ein prädikatenlogisches System LPL, das nur monadische Formeln enthält, endliche Modelle
wird als Monadische Prädikatenlogik bezeichnet. monadische einstellige Prädikate • Entscheidbarkeit der
Prädikatenlogik Î einfache Syllogismen Unerfüllbarkeit / Gültigkeit
Theoreme der monadischen Prädikatenlogik (Klassenlogik) Î Ergänzungsfragen behandelbar • Erfüllbare Formeln haben
endliche Modelle
1. Falls F eine Formel einer monadischen Prädikatenlogik ist, so gilt: Prädikatenlogik Prädikate beliebiger Stelligkeit • Semi-Entscheidbarkeit der
F ist erfüllbar genau dann, Unerfüllbarkeit / Gültigkeit
wenn F erfüllbar ist in einem Modell dessen Domäne maximal 2k r Elemente enthält, Î komplexe Syllogismen
Î Ergänzungsfragen behandelbar • Erfüllbare Formeln haben
wobei k die Anzahl der einstelligen Prädikate in F und r die Anzahl der Variablen in F ist. abzählbare Modelle
2. Es gibt ein Entscheidungsverfahren für die Erfüllbarkeit der monadischen Prädikatenlogik.
• (1) korrespondiert zum Theorem von Löwenheim-Skolem:
Jede erfüllbare Formel der Prädikatenlogik besitzt ein abzählbares Modell.
• (2) ist ein Konsequenz von (1).

Habel / Eschenbach Logik–13 [13] Habel / Eschenbach Logik–13 [14]

Logiken: Ausdruckskraft und Berechnungseigenschaften (2) Logik für InformatikerInnen: Jenseits von F1

• Grössere Ausdruckskraft führt – häufig – zu ungünstigeren Berechnungseigenschaften

• Entscheidbarkeit → Semi-Entscheidbarkeit (Effektivität) • Aussagenlogik & Prädikatenlogik: weitere Kalküle
• endliche Modelle → abzählbare Modelle
• Erweiterung der Ausdruckskraft logischer Sprachen
• Komplexität der Berechnungsverfahren (Effizienz)
• Modallogiken
Î Welche Ausdruckskraft benötigt wird, hängt vom Anwendungsgebiet ab! • Zeit-Logik
• nicht-monotone Logiken
• mehrwertige Logiken

• Was bleibt – in diesem Dilemma – zu tun? • Verbesserung der Berechnungseigenschaften

• Wähle die billigste Logik, die das Anwendungsgebiet zulässt, • terminologische Logik
z.B. suche monadische Teilbereiche. • Sortenlogik
• Suche effiziente Verfahren für spezifische Formelklassen • effiziente Schlussverfahren für spezifische Formelklasse
z.B. Hornlogik, Logik-Programmierung, eingeschränkte Resolutionsverfahren.
• Strategien des Schliessens
• Untergliedere die Menge der Terme! [→ Sortenlogiken]
• Berücksichtige Strukturen der Domäne! [→ temporale Logiken]

Habel / Eschenbach Logik–13 [15] Habel / Eschenbach Logik–13 [16]