Rechnergestütztes Beweisen
| Datum |
Vorlesung oder Übung |
Folien/Skript |
| Mi
| 19.10.
| VL 1
| Einführung
| contents.txt
vl1.txt
| | Do
| 20.10.
| VL 2
| Sequenzenkalkül
| vl2.txt
| | Do
| 20.10.
| Ü 1
| Sequenzenkalkül, PVS
|
| | Mi
| 26.10.
| VL 3
| Resolution
| vl3.txt
|
| Do
| 27.10.
| Ü 2
| Klauselgenerierung und Resolution
|
|
| Do
| 27.10.
| VL 4
| DPLL, Prädikatenlogik
| vl4.txt
| | Mi
| 02.11.
| VL 5
| Prädikatenlogik: Semantik und Sequenzenkalkül
| vl5.txt
|
| Do
| 03.11.
| Ü 3
| zChaff, FOL in PVS
|
|
| Do
| 03.11.
| VL 6
| Sequenzenkalkül: Korrektheit, Vollständigkeit
| vl6.txt
| | Mi
| 09.11.
| VL 7
| Satz von Herbrand, Unifikation, Resolution
| vl7.txt
|
| Do
| 10.11.
| Ü 4
| Logik erster Stufe in PVS
|
|
| Do
| 10.11.
| VL 8
| Kompaktheitssatz, Gleichheit
| vl8.txt
| | Mi
| 16.11.
| Ü 5
| Unifikations-Algorithmus; Gleichheit in PVS
|
|
| Do
| 17.11.
| VL 9
| ausgefallen
|
|
| Do
| 17.11.
| VL 10
| Rekursion
| vl10.txt
| | Mi
| 23.11.
| VL 11
|
|
|
| Do
| 24.11.
| Ü 6
| ausgefallen
|
|
| Do
| 24.11.
| VL 12
| Induktive Beweise fuer Listen: Filter, Reverse.
Datentypen in PVS
|
| | Mi
| 30.11.
| VL 13
| Gleichungstheorie, universelles Modell, Konvexität
| vl13.txt
|
| Do
| 01.12.
| Ü 7
| Induktive Beweise
|
|
| Do
| 01.12.
| VL 14
| Entscheidung durch Kanonisierung
| vl14.txt
| | Mi
| 07.12.
| VL 15
| Entscheidungsverfahren: Ackermann, Nelson-Oppen
| vl15.txt
|
| Do
| 08.12.
| Ü 8
| Semantische Normalisierung, Mergesort
|
|
| Do
| 08.12.
| VL 16
| Entscheidungsverfahren: Gleichungslösen, Shostak Light
| vl16.txt
| | Mi
| 14.12.
| VL 17
| Konstruktives Natürliches Schließen
|
|
| Do
| 15.12.
| Ü 9
| Propositionale Logik in Coq
|
|
| Do
| 15.12.
| VL 18
| Beweisreduktion, normale Beweise
| nd.ps
| | Mi
| 21.12.
| VL 19
| Konvexität II; Fallstudie Addierer
| vl19.txt
adder.pvs
|
| Do
| 22.12.
| Ü 10
| Entscheidungsverfahren; Coq
|
|
| Do
| 22.12.
| VL 20
| Fallstudie: Pipelined ALU
| vl20.txt
Dateien
| | Mi
| 11.01.
| VL 21
| Model checking
| vl21.txt
sem_finite.pvs
|
| Do
| 12.01.
| Ü 11
| CTL und Fixpunkte
| ue11.txt
|
| Do
| 12.01.
| VL 22
| Abstraktion und Model Checking
| vl22.txt
| | Mi
| 18.01.
| VL 23
| Abstraktion für Lebendigkeitseigenschaften
| vl23.txt
|
| Do
| 19.01.
| Ü 12
| CTL und Model Checking
| ue12.txt
|
| Do
| 19.01.
| VL 24
| Abhängige Typen
| vl24.txt
vl24.v
| | Mi
| 25.01.
| VL 25
| Natürlichen Schliessen für ∀, &exists; und induktive Typen
| vl25.txt
vl25.v
|
| Do
| 26.01.
| Ü 13
| FOL und Induktion in Coq
|
|
| Do
| 26.01.
| VL 26
| Induktive Familien und Gleichheit in der Typentheorie
| vl26.txt
vl26.v
| | Mi
| 01.02.
| VL 27
| Propositionale und Definitionale Gleichheit
| vl27.v
|
| Do
| 02.02.
| Ü 14
| Beweise in Coq; Induktive Beweise
|
|
| Do
| 02.02.
| VL 28
| Coq: Primzahlzertifikat und Vierfarbensatz
|
| | Mi
| 08.02.
| VL 29
| Klausur
|
|
| Do
| 09.02.
| Ü 15
| Nachholtermin Klausur
|
|
| Do
| 09.02.
| VL 30
| Besprechung der Klausur
|
|
Historischer Beweisbegriff, Mengentheorie als Formalisierung der Mathematik, Aufgaben und Verwendung
eines Beweispruefers (Theorembeweisers) Syntax und Semantik der Aussagenlogik.
Nach oben.
Regeln des Gentzen'schen Sequenzenkalküls, Korrektheit und Vollstaendigkeit, Sequenzen in PVS.
Nach oben.
- Exkurs: Lineare Logik
- Exkurs: Schnittelimination
- Resolution: Klauseln und -generierung, Resolutionsregel, Korrektheit und Vollständigkeit, Kompaktheit
Nach oben.
- Davis-Putnam Logemann-Loveland: Erfüllbarkeitsprozedur (SAT-Solver)
- Untypisierte Prädikatenlogik
- Typisierte Prädikatenlogik: Syntax (formal)
Nach oben.
- Interpretation von Termen und Formeln
- Beispiele von Tautologien
- Sequenzenkalkül
Nach oben.
- Korrektheit des Sequenzenkalküls
- Vollständigkeit des Sequenzenkalküls
Nach oben.
- Satz von Herbrand
- Unifikation für Terme erster Stufe
- Resolution für Logik erster Stufe
- Pränex-Form
Nach oben.
- Beispiel für Pränexform, Skolemisierung, Resolution
- SPASS
- Kompaktheitssatz und Nicht-Standard Modelle der Arithmetik
- Gleichheit: Syntax, Semantik und Sequenzenkalkül
- Gleichheit in PVS
Nach oben.
Es wurde gezeigt, dass jede in einer Gleichungstheorie ware Aussage allein mit den Gleichheitsregeln hergeleitet werden kann: Reflexivität, Symmetrie, Transitivität, Kongruenz und Substitution.
Kanonisierung durch semantische Auswertung (ausführlich) und
Termersetzung (oberflächlich). Rückführung von propositionalen
Gleichungsproblemen auf solche in Sequenzenform.
Nach oben.
- Disjunktionseigenschaft
- Brouwer-Heyting-Kolmogorov-Interpretation
- Natürliches Schliessen
- Beweisterme
Nach oben.
- Herleitbare und zulässige Regeln
- Abschwächungslemma und Substitutionslemma (induktive Beweise)
- Beweisreduktionen
- Normale Beweise für das Konjunktiv-Implikative Fragment
Nach oben.
- Eine konvexe Theorie hat ein universelles Modell
- Fallstudie PVS: Verifikation eines Addierwerks
adder.pvs
Nach oben.
- Fallstudie PVS: Verifikation einer Pipelined ALU:
.pvs-Dateien
- Weihnachtsfeier
Nach oben.
- Model checking im Allgemeinen: endliche Modelle
- Uninteressant für Logik erster Stufe und zu komplex für Logik höherer Stufe
- CTL (Computational Tree Logic)
- Bespiel: sem_finite.pvs
- μ-Kalkül
Nach oben.
- Unendliche Zustandsräume: Finde endliche Abstraktion
- Sicherheitseigenschaften und Abstraktion
- Halbautomatische Abstraktion in PVS: (abstract-and-mc)
Nach oben.
Nach oben.
- Demo der Diplomarbeit von Axelsson: Lebendigkeitseigenschaft mit Abstraktion (Bakery-Protokoll)
- Erweiterung des Curry-Howard-Isomorphismus auf Logik erster Stufe
- Abhängige Typen in Coq
- Die Universen Set und Prop
Nach oben.
- Einführungs- und Beseitigungsregeln für universelle und existentielle Quantifikation
- Reduktionen
- Arithmetik (natürliche Zahlen)
- Rekursionskombinator rec_nat
- Listen
- Implizite Argumente
Nach oben.
- Injektivität und Unterscheidung für Konstruktoren
- Induktive Familie der Vektoren
- Induktive Relation: Kleiner-gleich
- Strukturelle Rekursion (Fixpoint) und Termination
- Positivitätsbedingung für induktive Typen
-
Nach oben.
- Primzahlzertifikate nach Pocklington
- George Gonthier's Beweis der Vierfarbentheorems in Coq
Nach oben.
Sequenzenkalkül, PVS
Material:
Nach oben.
Verbesserung der Übungen zu Sequenzenkalkül und logischen Rätseln in
PVS. Vorstellung eines Algorithmus zur Klauselgenerierung;
Resolution.
Nach oben.
Verbesserung von Blatt 2. Beweis der Korrektheit des
Klauselgenerierungsalgorithmusses. zChaff Mini-Tutorial. FOL-Beweise in PVS.
Material:
Nach oben.
Verbesserung von Blatt 3:
- Erläuterung zu den Seq.kalkülsregeln für Quantoren: Dynamische Spracherweiterungen, Instantiierung
- Formalisierungsalternativen (für Supremum etc.)
- PVS-Beweise mit
lemma und expand.
- SPASS Demo
- Pränexform und Skolemisierung
Material:
Nach oben.
Verbesserung von Blatt 4:
- Pränex-Form, Skolemisierung, Resolution
- Substitutions-Monoid und Quasi-Ordnung auf Substitutionen
- Allgemeinster Unifikator durch schrittweise Vereinfachung: Korrektheit und Vollständigkeit
- Formalisierung einer Gruppe in PVS
- PVS-Beweise mit
replace und rewrite.
Material:
Nach oben.
- Primitive Rekursion
- Verbesserung von Blatt 6: Korrektheit von Insertion Sort in PVS
- Vorbesprechung zu Blatt 7: Merge Sort
- Verlaufsrekursion und spezielle Induktionsschemata
measure-induct+
Material:
Nach oben.
- Semantische Normalisierung (Norm. durch Auswertung) am Beispiel der Theorie der Paare und Projektionen.
- Korrektheit von Mergesort.
Material:
Nach oben.
Material:
Nach oben.
Verbesserung von Blatt 9:
- Konvexität der linearen Arithmetik
- Nicht-Standard Modell der Booleans (mit Bottom)
- Nelson-Oppen und Shostak light Entscheidungsprozeduren
- Taktiken für propositionale Logik
- Beweisterme in Coq
Material:
Nach oben.
Verbesserung von Blatt 10:
- Korrektheit der pipelined ALU für stalled=true
- Spezifikation des Multiplizierwerks
- Unbewiesene Hilfslemmata
- Beweis der Korrektheit des Multiplizierwerks
Übungen zur VL 21 (Protokoll von Robert Noll liegt vor):
- CTL Formeln und Beispiele dazu
- Fixpunkte: Bespiele für kleinsten und größten Fixpunkt
- Beweis, dass Schnitt aller Präfixpunkte der kleinste Fixpunkt ist
Material:
- loesung-b10.zip Lösung Blatt 10 (enthält Lösung von Ulrich Schöpp
us_mult.p?? und den in der Übung vorgeführten Beweis des Hauptlemmas aa_mult.p??)
- ue11.txt Übungsprotokoll
Nach oben.
Verbesserung von Blatt 11:
- Übersetzung natürlichsprachlicher Aussagen in CTL
- Äquivalenz der Fixpunktdef. "von unten" und "von oben"
- Modellierung des Alternating Bit Protocols in PVS
Material:
Nach oben.
- Universelle und existentielle Quantifikation in Coq
- Taktiken: intro, apply, assert, induction, inversion, constructor.
Material:
Nach oben.
|
Andreas Abel
Last modified: Wed Feb 8 16:12:23 CET 2006
|
|
|