Ist doch Logisch

Jetzt loslegen. Gratis!
oder registrieren mit Ihrer E-Mail-Adresse
Rocket clouds
Ist doch Logisch von Mind Map: Ist doch Logisch

1. Aussgenlogik

1.1. Allgemein

1.1.1. Sehr beschränkte Logik

1.1.2. Vieles nicht aussagbar

1.1.3. Logische Verknüpfung mittels Junktoren nicht, und, oder

1.2. Atomare Formeln

1.2.1. Wahrheitswerte oder Variablen

1.3. Syntax

1.3.1. Beschreibt wie Formeln zusammengesetzt werden können

1.3.2. Induktiv definiert

1.4. Semantik

1.4.1. Bedeutung

1.4.2. Wahrheitstabelle: Wie die einzelnen Zeilen erstellt werden

1.4.3. Es gibt eine Belegung (Funktion)

1.4.3.1. Regeln legen fest wie die Fuktion rechnet

1.4.4. Wenn 1 rauskommt, erfüllt die Belegung die Formel: V |= phi.

1.4.4.1. V ist ein Modell von phi

1.5. Junktoren

1.6. Koinzidenzlemma

1.6.1. var(phi) die variablen die in Formel phi vorkommen

1.6.2. Sei phi Formel und V1, V2 Belegungen mit V1(x) = V2(x) für alle x, dann sind die beiden gleich V1(phi) = V2(phi)

1.7. Auswertungsproblem

1.7.1. Gegeben: AL phi und Belegung V. Frage: Gilt V(phi) = 1?

1.7.2. In linearzeit Lösbar

1.7.3. Vorgehen: Rekursiv alle Teilformen auswerten

1.8. Kompaktheitssatz

1.8.1. Eine Menge von AL ist genau dann erfüllbar, wenn jede endliche Teilmenge erfüllbar ist.

1.9. Äquivalenz

1.9.1. Idempotenz

1.9.2. Kommutativität

1.9.3. Assoziativität

1.9.4. Absorption

1.9.5. Distributivgestöätz

1.9.6. Doppelnegation

1.9.7. De Morgansche Regel

1.9.8. Tautologieregeln

1.9.9. Unerfüllbarkeitsregeln

1.10. Ersetzungsllemma

1.10.1. F1,F2 zwei Äquivalente Formeln, G eine in der F1 als Teilformel vorkommt. Sei G' die Formel die man erhält wenn man G in F1 durch F2 ersetzt. Dann: G=G'

1.10.2. Äquivalente Formeln sind austauchbar

1.11. Boolsche Funktionen

1.11.1. Fkt mit >= 1 boolschen Parametern die einen boolschen Wahrheitswert zurückgibt

1.11.2. Jede Aussagenlogische Formel phi, mit |Var(phi)| = n berechnet n-stellige boolsche-Fkt Fi

1.12. Normalformen

1.12.1. Konjunktive

1.12.2. Disjunktive

1.12.3. jede ALF kann in KNF/DNF gewandelt werden

1.13. Funktionale Vollständigkeit

1.13.1. Um alles ausdrücken zu können, braucht man nicht alle Junktoren.

1.13.2. nicht & und reichen, weil man das oder mit und/nicht darstellen kann

1.14. Erfüllbarkeit

1.14.1. Erfüllbar = die Formel phi hat ein Modell

1.14.2. Erfüllbarkeitsproblem

1.14.2.1. Gegeben: Formel F. Frage: Gibt es eine Belegung V, die ein Modell von F ist?

1.14.2.2. NP-Vollstaendig

1.14.3. Eine Menge von Formeln heißt erfüllbar, wenn mindestens eine ein Modell besitzt

1.15. Gültigkeit

1.15.1. Gültig = Tautologie = alle möglichen Belegungen sind ein Modell

1.15.2. Naiver Algorithmus: Zähle alle 2^n Belegungen auf und Prüfe

1.15.3. co-NP-vollständig

1.15.4. In KNF liearzeit

1.16. Dualität von Erfüllbarkeit/Gültigkeit

1.16.1. phi gültig, wenn nicht phi unerfüllbar ist

1.16.2. phi erfüllbar, wenn nicht phi gültig ist

1.17. Folgerbarkeit

1.17.1. Eine Formel psi ist folgerbar aus einer anderen Formel phi gdw. für alle Belegungen V mit V |= phi ist auch V |= psi

1.17.2. Schreibweise: phi |= psi (aus phi folgt psi. psi ist Konsequenz von phi)

1.17.3. Modus Ponens

1.17.3.1. phi UND (phi -> psi) |= psi

1.17.3.2. Aus: Es regnet (phi) UND Wenn es regnet, wird die Straße nass (phi -> psi), folgt: Straße ist nass (psi)

1.17.4. Beispiel: x UND y |= x

1.17.4.1. Alle Belegungen die auf der linken Seite Wahr ergeben, müssen auch rechts wahr sein.

1.18. Hornformeln

1.18.1. Formel in KNF, wobei jede Disjunktion höchstens 1 Positives Literal enthält

1.18.2. Erfüllbarkeit in linearzeit

1.18.3. Ausdrückbarkeit

1.18.3.1. x OR y -> z

1.18.3.2. nicht ausdrückbar: x OR y

1.19. Resolutionskalkül

1.19.1. Kalkül: Rechenregeln zum umformen der Formel

1.19.2. Resolutionskalkül

1.19.2.1. Kalkül zum entscheiden der unerfüllbarkeit von ALF in KNF

1.19.2.2. wegen Dualität auch Tautologie prüfbar

1.19.2.3. Klauselmenge aus KNF erstellen

1.19.2.4. Resolvente

1.19.2.4.1. Anschaulich: Wenn in F1 eine var positiv und in F2 negativ vorkommt, kann man die streichen. rest ist die Resolvente

1.19.2.4.2. K1, K2, K3 Klauseln. K3 Resolvente von K1 und K2, wenn es in K1 ein Literal postiv gibt, welches in K2 negativ ist

1.19.2.4.3. K3 = K1\{L} U K2\{neg L}

1.19.2.5. Resolutionslemma

1.19.2.5.1. F AL, K(F) Klauselmenge. K3 Resolvente von K1, K2. F ist äquivalent zu K(F) U {K3}

1.19.2.5.2. Wir können die Resolvente zur Formel hinzufügen und verändern damit die Formel nicht

1.19.2.6. Resolutionssatz

1.19.2.6.1. Eine Formel F unerfüllbar gdw leere Menge in Res^∞ (K(F)) gilt.

1.19.2.6.2. Also wenn die leere Menge als Resolvente rauskommt

1.19.2.6.3. Abbruchbedingung: 1. leere Menge kommt raus 2. Es fällt nichts mehr weg, es ändert sich nichts

1.19.2.7. Resolutionsschritte

1.19.3. Aufwand

1.19.3.1. NP

1.19.3.2. Es gibt spezialtypen von Formeln mit denen Berechnung in polynomieller Zeit möglich ist -> Horn-Formeln

1.20. Einheitsresolution

1.20.1. Einheitsresolvente:

1.20.1.1. Wenn ein Literal aus denen man die Resolvente macht nur ein Literal hat

1.20.1.2. Wenn leere Menge bei Einheitsresolution rauskommt, ist Horn-Formel unerfüllbar

1.21. Hilbert-Kalkül

1.21.1. Alle gültigen Formeln erzeugen

1.21.2. Gibt so Schlussfolgerungsregeln

2. Allgemein

2.1. Logisches System

2.2. Anwendung von Logik

2.2.1. Automatische Beweise

2.2.2. KI

2.2.3. Datenbanken

3. Algorithmen

3.1. Aussagenlogik

3.1.1. Auswertungsproblem Linearzeit / Polyzeit

3.1.2. Erfüllbarkeitsproblem NP-vollständig

3.1.3. Gültigkeitsproblem co-NP-vollständig

3.1.4. Gültigkeitsproblem für KNF/DNF Linearzeit

3.1.5. Folgerbarkeitsproblem co-NP-vollständig

3.1.6. Hornformeln

3.1.6.1. Erfüllbarkeitsproblem Linearzeit

3.1.7. Resolutionskalkül Erfüllbarkeit: NP (2^n)

3.2. Prädikatenlogik

3.2.1. Auswertungsproblem PSpace-vollständig

3.2.2. Entscheidungsproblem Nicht entscheidbar

3.2.3. Erfüllbarkeitsproblem

3.2.4. Gültigkeitsproblem

4. Prädikatenlogik

4.1. Allgemein

4.1.1. Erweitert die AL um Quantoren

4.1.2. Aussagen über unendliche Mengen treffen

4.1.3. Mächtiger aber mehr Komplexität

4.2. Syntax

4.2.1. Variable

4.2.2. Funktion

4.2.2.1. stelligkeit = anzahl der parameter

4.2.2.2. Hat rückgabewert (wert oder variable)

4.2.3. Prädikat/Relation

4.2.3.1. Aussgage / Kein Rückgabewert

4.2.3.2. z.B. even, >, "x ist beliebt bei y"

4.2.4. Term

4.2.4.1. induktiv

4.2.4.1.1. Sei S eine Signatur. Die Menge T(S) der S-Terme ist dann: VAR [Teilmenge von] T(S) sind t_1,...,t_n € T(S) und f € F^n(S), dann ist auch f(t_1,...,t_n) € T(S)

4.2.5. Prädikatenlogische Formel

4.2.5.1. induktiv

4.2.5.1.1. Einzelne VARs sind eine Formel. Verundete und vernichtete, ... sind dann auch Formeln

4.2.6. Teilformel

4.2.6.1. Wie Aussagenlogitk

4.2.7. freie/gebundene Variabel

4.2.7.1. kommt x in einer Teilformel forall x: G oder exists x: G vor, so heißt x gebunden, sonst frei

4.3. Semantik

4.3.1. Zuweisung/Interpretation

4.3.1.1. Ein Paar (A, ß) mit Zuweisung ß in A heisst Interpretation

4.3.1.2. Wie vorher bei AL die Belegung

4.3.2. Struktur

4.3.2.1. Besteht aus nichtleerem Universum A und Interpretsfkt

4.3.3. Signatur

4.3.3.1. Die Namen

4.3.3.2. Aus diesen Namen kannste Fkt und Relationen basteln

4.3.4. Erfülltheitsrelationen

4.3.4.1. das Zeichen |=

4.4. Koinzidenzlemma

4.4.1. Analog zur AL

4.4.2. Erlaubt uns nur die freien Variablen zu betrachten

4.5. Isomorphielemma

4.5.1. Isomporphie=Gleichheit

4.5.2. Zwei Strukturen sind gleich, außer dass man Elemente des Universums umbenennen muss

4.6. Auswertungsproblem

4.6.1. exponentiell viel Zeit: NP

4.6.2. PSpace-vollständig

4.6.3. Algorithmus rekursiv die einzelnen Teilformeln

4.7. Äquivalenzen

4.7.1. Analog zu Al

4.7.2. Zusätzlich

4.7.2.1. Dualität von forall, exists

4.7.2.2. Distrubutiv für forall, exsits

4.8. Domänenunabhängigkeit

4.8.1. Gültig in allen Domänen

4.9. FO und Datenbanken

4.9.1. Datenbankinstanz = relationale Struktur

4.9.2. Übersetzung FO->SQL benötigt nur linear zeit

4.9.3. FO in der Ausdrücksstärke = SQL-Kern

4.10. Ersetzungslemma

4.10.1. wie AL

4.11. Reduzierte FO-Formel

4.11.1. Formel hat nur Junktoren neg, UND und den Quantor exists

4.12. Erfüllbar/Gültig/Konsequenz

4.12.1. wie AL

4.13. Normalformen

4.13.1. Negations-Normalform

4.13.1.1. Wenn in einer Formel Negationenn ur auf Atome angewendet werden

4.13.1.2. Jede Formel kann in linearzeit in NNF gewandelt werden

4.13.2. Pränex-Normalform

4.13.2.1. bereinigt

4.13.2.1.1. Keine Variable tritt sowohl frei als auch gebunden auf

4.13.2.1.2. Keine Variable wird mehr als einmal quantifiziert

4.13.2.1.3. Jede Formel kann in linearzeit bereinigt werden

4.13.2.2. Formel ist in Pränex-Normalform, wenn

4.13.2.2.1. Formel-Bereinigt

4.13.2.2.2. Alle Quantoren vorne stehen

4.14. Unentscheidbarkeit Prädikatenlogik

4.14.1. endliche Gültigkeit, Erfülbarkeit, Konsequenz sind unentscheidbar in FO

4.15. Positives zu berichten

4.15.1. Gültige Formeln sind rekursiv aufzählbar

4.15.2. Syntaktische-Einschränkungen liefern Entscheidbarkeit

4.16. FO-Theorien

4.16.1. Goldbachsche Vermutung

4.16.2. Presburger Arithmetik

4.16.3. Skolem Arithmetik

4.16.4. Artihmetik der reellen Zahlen

4.16.5. arithmetik der natürlichen Zahlen

4.16.6. Axiomatisierung

4.17. Sequenzenkalkül

4.17.1. Allgemein

4.17.1.1. Kalkül für Gültigkeit

4.17.1.2. Zum Ableiten aller Tautologien / unerfüllbaren Formeln

4.17.2. Def./Syntax Sequenz

4.17.2.1. Ausdruck der Form Γ -> Δ

4.17.2.2. Γ = Antezendenz

4.17.2.3. Δ = Sukzedenz

4.17.3. FO Satz

4.17.3.1. Tautologie wenn ∅ -> {phi}

4.17.3.2. Unerfüllbar wenn {phi} -> ∅

4.17.4. Schlussregeln. 2 Stk pro Junktor

4.17.5. SK-Beweis

4.17.5.1. Baum

4.17.5.2. Jede ableitbare Sequenz ist gültig

4.17.6. Wichtigste Anwendung: Beweis der Kompaktheit von Fo

4.18. Rekursive Aufzählbarkeit

4.18.1. endliche Strukturen

4.18.1.1. Die Menge der erfüllbaren Formeln ist rekursiv aufzählbar für jede aufzählbare Signatur Tau

4.18.2. unendliche Strukturen

4.18.2.1. Für jede aufzählbare Signatur Tau sind rekursiv aufzählbar:

4.18.2.1.1. Die Menge aller Tautologie aus FO(Tau)

4.18.2.1.2. Die Menge aller unerfüllbaren Formeln aus FO(tau)

4.18.2.2. Wenn Tau mind. ein binäres Relationssymbol enthält ist die Menge der erfüllbaren FO-Formeln nicht aufzählbar

4.18.3. Rekursive Aufzählung liefert Semi-Entscheidbarkeit für Gültigkeit

4.19. Löwenheim/Skolem

4.19.1. Alles was n endliches Modell hat, hat auch n unendliches

4.19.2. Überabzählbarkeit/Abzählbarkeit ist nicht FO-Ausdrückbar

4.20. Ausdrückbarkeit

4.20.1. Eigenschaft die nicht unter isomophie abgeschlossen ist NICHT FO-ausdrückbar

4.20.2. Zusammenhang von ungerichteten Graphen ist nicht ausdrückbar

4.20.3. Ehrenfeucht-Fraisse-Spiele

4.20.3.1. Erlauben nicht-ausdrückbarkeit von Eigenschaften als FO-Formel

4.20.3.2. Zwei Spieler: Spoiler (beginnt), Duplikator

4.20.3.3. Spielfeld 2 Tau-Strukturen

4.20.3.4. jeder Spieler zieht abwechselnd

4.20.3.5. Wenn Spoiler aus A zieht, muss Duplikator aus B, und umgekehrt

4.20.3.6. k Schritte, vorher festgelegt

4.20.3.7. Wenn die Menge nach k Schritten ein partieller Isomorphismus ist, gewinnt Duplikator

4.20.3.8. Gewinnstrategie: Wenn einer gewinnen kann, ohne das der andere was dagegen machen kann

4.20.3.9. Zusammenhang EF und FO

4.20.3.9.1. Abwechselnde Züge entsprechen Quantorenalterniereungen

4.20.3.9.2. Duplikator hat Gewinnstrategien wenn Strutur A und Struktur B jeweils Formel phi erfüllen (A |= phi und B |= phi)

4.20.3.9.3. Wenn wir zeigen wollen, dass eine Sache/Eigenschaften nicht in FO ausdrückbar ist, müssen wir zeigen, dass der Duplikator für jedes k>=0 eine Gewinnstrategie hat.

5. Logik zweiter Stufe

5.1. Man kann auch über Mengen von Elementen und Relationen quantifizieren

5.2. Transitive Hülle oder even sind ausdrückbar

5.3. erfüllt nicht Kompaktheitseigenschaft

5.4. Abzählbarkeit und überabzählbarkeit ausdrückbar

5.5. MSO

5.5.1. nur unäre Relationssymbnole

5.5.2. Zusammenhang von Graphen ausdrückbar

5.5.3. für praktischen Einsatz zu langsam

5.6. Auswertung von SO/MSO

5.6.1. polynomiell viel Platz für MSO

5.6.2. exponentiell viel Platz für SO

5.6.3. MSO: Pspace-vollständig

5.6.4. SO. Exspace-vollständig

5.7. MSO über linearen Strukturen

5.7.1. MSO entscheidbar über eingeschränkte Strukturklassen

5.7.1.1. endliche und unendliche Strukturklassen

5.7.1.2. endliche und unendliche Baumstrukturen

5.7.1.2.1. Worte im Sinne der formalen Sprache

5.8. S1S-Struktur

5.8.1. Wörter über €_n

5.9. Temporallogik

5.9.1. LTL,CTL,µ-Kalkül

5.9.2. LTL

5.9.2.1. Neue Quantorenzeichen: O, ◊ ,□,Until

5.10. Die in SO definierbaren Entscheidungsprobleme sind exakt die NP-Probleme