Toggle navigation
Home
Videos
FAQ
Zur neuen Seite
Algorithmische Modelltheorie
Semester:
Wintersemester 2019/20
Veranstalter:
Prof. Grädel
Bemerkungen:
Webseite der Vorlesung: https://www.logic.rwth-aachen.de/Teaching/AMT-WS19/index.html.de
Videos
Vorlesung
Di, 08.10.2019, 08:30 Uhr
Das klassische Entscheidungsproblem
Grundbegriffe über Entscheidbarkeit
Rekursive Untrennbarkeit
Verfeinerungen von H-epsilon
Satz (paarweise rekursive Untrennbarkeit von Hε⁺, Hε⁻, Hε^∞)
Download
1080p (1.2 GiB)
720p (612.1 MiB)
360p (312.9 MiB)
1080p (1.2 GiB)
720p (612.1 MiB)
360p (312.9 MiB)
Vorlesung
Mo, 14.10.2019, 10:30 Uhr
Fortsetzung (rekursive Untrennbarkeit von Hε⁺, Hε⁻)
Satz von Trakhtenbrot vorbereitung
Satz (Entscheidbarkeit, falls FMP)
Satz von Trakhtenbrot
(konservative) Reduktionsklassen
Klassifikationssatz
Download
1080p (1.2 GiB)
720p (644.5 MiB)
360p (359.2 MiB)
1080p (1.2 GiB)
720p (644.5 MiB)
360p (359.2 MiB)
Vorlesung
Di, 15.10.2019, 08:30 Uhr
Domino Probleme
Satz (Berger & Robinson)
Satz (Paketierung ℕ×ℕ erweitert auf ℤ×ℤ)
Satz (rekursiv untrennbare Dominoprobleme)
Anwendungen der Domino Methode
Satz (KMW ist konservative Reduktionsklasse)
Definition (FOᵏ)
Satz (konservative Reduktionsklasse funktionaler Signaturen und ∀)
Download
1080p (1.1 GiB)
720p (602.2 MiB)
360p (332.8 MiB)
1080p (1.1 GiB)
720p (602.2 MiB)
360p (332.8 MiB)
Vorlesung
Mo, 21.10.2019, 10:30 Uhr
Die Endliches-Modell-Eigenschaft (FMP)
Definition (atomarer k-Typ)
Satz (MFO hat FMP)
FO²
Lemma (Scott)
Geschichte (Gödels Fehler)
Satz (FO² hat FMP)
Beispiel (Hofstaat, endliches Modell)
Download
1080p (1.3 GiB)
720p (700.4 MiB)
360p (387.7 MiB)
1080p (1.3 GiB)
720p (700.4 MiB)
360p (387.7 MiB)
Vorlesung
Di, 22.10.2019, 08:30 Uhr
Fortsetzung (FO² hat FMP)
Komplexität von Sat(FO²)
Domino(D,T)
Lemma (Reduktion von 2ⁿ-Domino auf FO² ∩ MFO ∩ „∀²∃“ ohne =)
Résumé (Entscheidungsproblem)
Download
Format unbekannt (3.3 GiB)
Format unbekannt (3.3 GiB)
Vorlesung
Mo, 28.10.2019, 10:30 Uhr
2. Deskriptive Komplexität
Beispiele für Deskriptive Komplexität
Definition (∑¹₁)
Kodierung
Definitionen (logische Charakterisierung von Komplexitätsklassen auf Bereichen)
Satz (Fagin)
Ausblick
Download
1080p (1.3 GiB)
720p (693.9 MiB)
360p (392.4 MiB)
1080p (1.3 GiB)
720p (693.9 MiB)
360p (392.4 MiB)
Vorlesung
Di, 29.10.2019, 08:30 Uhr
Fortsetzung (Satz von Fagin)
Satz (Cook & Levin)
Definition (SO-HORN, ∑¹₁-HORN)
Satz (∑¹₁-HORN entspricht SO-HORN)
Satz (SO-HORN liegt in PTIME)
Download
1080p (1.3 GiB)
720p (698.5 MiB)
360p (386.0 MiB)
1080p (1.3 GiB)
720p (698.5 MiB)
360p (386.0 MiB)
Vorlesung
Mo, 04.11.2019, 10:30 Uhr
Satz (Grädel)
3. LFP und infinitäre Logik
Fixpunkttheorie / Ordinale
Satz (Knaster & Tarski)
Satz (induktive Konstruktion)
Download
1080p (1.3 GiB)
720p (692.8 MiB)
360p (387.2 MiB)
1080p (1.3 GiB)
720p (692.8 MiB)
360p (387.2 MiB)
Vorlesung
Di, 05.11.2019, 08:30 Uhr
Dualität
Berechenbarkeit (lfp und gfp in PTIME)
Definition (LFP)
Beispiele (LFP-Formeln)
Komplexität von LFP
Negationsnormalform für LFP
Beispiel (Bisimulation als gfp)
Ausblick (LFP ≠ PTIME)
Download
1080p (1.3 GiB)
720p (674.7 MiB)
360p (387.2 MiB)
1080p (1.3 GiB)
720p (674.7 MiB)
360p (387.2 MiB)
Vorlesung
Mo, 11.11.2019, 10:30 Uhr
Beobachtung (LFP liegt in SO)
Satz (SO-HORN liegt in LFP)
Résumé (LFP vs. PTIME)
Definition (infinitäre Logiken)
Download
1080p (1.3 GiB)
720p (709.3 MiB)
360p (402.8 MiB)
1080p (1.3 GiB)
720p (709.3 MiB)
360p (402.8 MiB)
Vorlesung
Di, 12.11.2019, 08:30 Uhr
4. FO auf endlichen Strukturen
Satz von Ehrenfeucht-Fraïssé
Hin- und Her-Systeme
Lemma (Charakterisierung von Hin- und Her-Systemen durch FO-Formeln)
Beweis (Satz von Ehrenfeucht-Fraïssé)
Lokalität von FO
Download
1080p (1.3 GiB)
720p (698.0 MiB)
360p (394.8 MiB)
1080p (1.3 GiB)
720p (698.0 MiB)
360p (394.8 MiB)
Vorlesung
Mo, 18.11.2019, 10:30 Uhr
Beispiel (Satz von Hanf)
Beweis (Satz von Hanf)
Satz von Gaifman
Beweis (Satz von Gaifman, via Lemma)
Kommentar (elementare Komplexität, Komplexität vs. Praxis)
Download
1080p (1.1 GiB)
720p (569.6 MiB)
360p (317.7 MiB)
1080p (1.1 GiB)
720p (569.6 MiB)
360p (317.7 MiB)
Vorlesung
Di, 19.11.2019, 08:30 Uhr
Beweis (zum Satz von Gaifman)
Beispiel (Satz von Gaifman)
Untere Schranke für die Länge lokaler Sätze
Download
1080p (1.3 GiB)
720p (679.9 MiB)
360p (389.5 MiB)
1080p (1.3 GiB)
720p (679.9 MiB)
360p (389.5 MiB)
Vorlesung
Mo, 25.11.2019, 10:30 Uhr
0-1-Gesetze
Download
1080p (1.3 GiB)
720p (698.1 MiB)
360p (396.4 MiB)
1080p (1.3 GiB)
720p (698.1 MiB)
360p (396.4 MiB)
Vorlesung
Di, 26.11.2019, 08:30 Uhr
Wurde nicht aufgezeichnet
Vorlesung
Mo, 02.12.2019, 10:30 Uhr
Satz (θk bestimmt Lk∞ω Formeln durch atomare Typen)
Konsequenz des 0-1-Gesetzes für LFP
6. Modale, inflationäre und partielle Fixpunktlogiken
Erinnerung (ML, Einbettung in FO², Bisimulationsinvarianz, Baummodelleigenschaft)
Definition (modaler µ-Kalkül)
Beispiele (Lµ-Formeln)
Einbettungen (von Lμ)
Download
1080p (1.3 GiB)
720p (692.2 MiB)
360p (393.4 MiB)
1080p (1.3 GiB)
720p (692.2 MiB)
360p (393.4 MiB)
Vorlesung
Di, 03.12.2019, 08:30 Uhr
Bisimulationsinvarianz (von Lμ)
Definition (inflationäre Fixpunktlogik IFP)
Komplexität von IFP
Beispiele (IFP-Formeln)
Stage Comparison Relationen
Beweis (IFP = LFP)
Definierbarkeit der Stage Comparison Relationen in IFP
Download
1080p (1.3 GiB)
720p (706.5 MiB)
360p (361.1 MiB)
1080p (1.3 GiB)
720p (706.5 MiB)
360p (361.1 MiB)
Vorlesung
Mo, 09.12.2019, 10:30 Uhr
sorgfältigere Erklärung der Stage Comparison Formel
Satz (Stage Comparison in posLFP)
Satz (LFP ≡ IFP)
Definition (Simultane Induktionen S-LFP)
Beispiel (S-LFP)
Definition (Partielle Fixpunktlogik PFP)
Beispiel / Komplexität von PFP
Download
1080p (1.1 GiB)
720p (597.6 MiB)
360p (305.4 MiB)
1080p (1.1 GiB)
720p (597.6 MiB)
360p (305.4 MiB)
Vorlesung
Di, 10.12.2019, 08:30 Uhr
Wurde nicht aufgezeichnet
Vorlesung
Mo, 16.12.2019, 10:30 Uhr
Definition (Fixpunktlogik mit Zählen FPC)
7. Fixpunktlogik mit Zählen
Beispiele (FO+C)
Definition (Fixpunktlogik mit Zählen FPC)
Beispiel (FPC)
Kommentar
Download
1080p (1.4 GiB)
720p (728.5 MiB)
360p (372.4 MiB)
1080p (1.4 GiB)
720p (728.5 MiB)
360p (372.4 MiB)
Vorlesung
Di, 17.12.2019, 08:30 Uhr
Vorlesung
Mo, 06.01.2020, 10:30 Uhr
Wiederholung (k-Bijektionsspiel)
CFI-Konstruktion
Satz (Charakterisierung der CFI-Graphen)
Lemma (lokale Charakterisierung bei gemeinsamen Knoten)
Lemma (einzelne Kanten)
Beweis (Charakterisierung der CFI-Graphen)
Satz (CFI-query ist in PTIME)
Ausblick (CFI-query ist nicht FPC-definierbar)
Download
1080p (1.4 GiB)
720p (730.9 MiB)
360p (373.6 MiB)
1080p (1.4 GiB)
720p (730.9 MiB)
360p (373.6 MiB)
Vorlesung
Di, 07.01.2020, 08:30 Uhr
Wurde nicht aufgezeichnet
Vorlesung
Mo, 13.01.2020, 10:30 Uhr
Vorlesung
Di, 14.01.2020, 08:30 Uhr
Vorlesung
Mo, 20.01.2020, 10:30 Uhr
Keine Vorlesung
Vorlesung
Di, 21.01.2020, 08:30 Uhr
Wurde nicht aufgezeichnet
Vorlesung
Mo, 27.01.2020, 10:30 Uhr
Metaendliche Modelltheorie
Download
1080p (1.3 GiB)
360p (350.4 MiB)
Format unbekannt (685.5 MiB)
1080p (1.3 GiB)
360p (350.4 MiB)
Format unbekannt (685.5 MiB)
×
Error