Rechnergestütztes Beweisen
H = Vorlesung Hofmann, A = Vorlesung Abel, Ü = Übung.
| Datum |
Vorlesung oder Übung |
Folien/Skript |
| Di
| 16.10.
| H 1
| Einführung
| contents.txt
vl01.txt
| | Mi
| 17.10.
| H 2
| Sequenzenkalkül
| vl02.txt
| | Mo
| 22.10.
| Ü 1
| Sequenzenkalkül, PVS
|
| | Di
| 23.10.
| H 3
| Resolution
| vl03.txt
|
| Mi
| 24.10.
| A 1
| Konstruktive Aussagenlogik und Beweisterme
| clskript.pdf
| | Mo
| 29.10.
| Ü 2
| Klauselgenerierung und Resolution
|
|
| Di
| 30.10.
| H 4
| DPLL; Prädikatenlogik: Semantik
| vl04.txt
skript-2007-10-30.ps
| | Mi
| 31.10.
| H 5
| Prädikatenlogik: Sequenzenkalkül, Korrektheit, Vollständigkeit
| vl05.txt
| | Mo
| 05.11.
| Ü 3
| zChaff, FOL in PVS
|
| | Di
| 06.11.
| A 2
| Beweisreduktion, normale Beweise
| red.ps
| | Mi
| 07.11.
| A 3
| Kripke-Modelle und Vollständigkeit des natürlichen Schließens
| kripke.ps
| | Mo
| 12.11.
| Ü 4
| Konstruktive Logik: Normalisierung und Gegenmodelle
|
| | Di
| 13.11.
| H 9
| Sequenzenkalkül: Vollständigkeit
| vl06.txt
| | Mi
| 14.11.
| H 10
| Satz von Herbrand, Resolution, Kompaktheit der Prädikatenlogik
| vl07.txt
| | Mo
| 19.11.
| Ü 5
| ausgefallen
|
| | Di
| 20.11.
| H 11
| Unifikations-Algorithmus; Gleichheit
| vl08.txt
| | Mi
| 21.11.
| H 12
| Induktive Beweise fuer Listen, Datentypen in PVS
| vl10.txt
| | Mo
| 26.11.
| Ü 6
| ausgefallen
|
| | Di
| 27.11.
| H 13
| Gleichungstheorie, universelles Modell, Konvexität
| vl13.txt
| | Mi
| 28.11.
| H 14
| Entscheidung durch Kanonisierung
| vl14.txt
| | Mo
| 03.12.
| Ü 7
| ausgefallen
|
| | Di
| 04.12.
| H 15
| ausgefallen
|
| | Mi
| 05.12.
| H 16
| ausgefallen
|
| | Mo
| 10.12.
| Ü 8
| Induktive Beweise in PVS
|
| | Di
| 11.12.
| H 17
| Entscheidungsverfahren: Ackermann, Nelson-Oppen
| vl15.txt
| | Mi
| 12.12.
| H 18
| Entscheidungsverfahren: Gleichungslösen, Shostak Light
| vl16.txt
| | Mo
| 17.12.
| Ü 9
| Fallstudie: Normalisierung von If-Ausdrücken
|
| | Di
| 18.12.
| H 19
| Konvexität II; Fallstudie Addierer
| vl19.txt
adder.pvs
|
| Mi
| 19.12.
| H 20
| Fallstudie: Pipelined ALU
| vl20.txt
Dateien
| | Mo
| 07.01.
| Ü 10
| Propositionale Logik in Coq
|
|
| Di
| 08.01.
| A 4
| Propositionale Logik in Coq
| 2008-01-08.v
| | Mi
| 09.01.
| A 5
| Konstruktive Prädikatenlogik, Kripke-Modelle
| Skript: ipl.ps
| | Mo
| 14.01.
| Ü 11
| Coq: Beweise über Funktionen und Relationen
|
| | Di
| 15.01.
| A 6
| Kripke-Modelle, Induktive Typen
| 2008-01-15.v
| | Mi
| 16.01.
| A 7
| Heterogene Datentypen, Positivität, Induktive Aussagen
| indProp.v
| | Mo
| 21.01.
| Ü 12
| Kripke-Modelle, Induktive Typen/Relationen
| ue9/deBruijn.v
| | Di
| 22.01.
| A
| Abhängige Typen
Induktive Familien und Gleichheit in der Typentheorie
| vl24.txt
vl24.v
vl25.txt
vl25.v
vl26.txt
vl26.v
| | Mi
| 23.01.
| H
| Entscheidungsprozeduren in Coq
| vl-coq-dec.txt
ring.v
| | Mo
| 28.01.
| Ü 13
| Induktive Familien in Coq
| loesung27-19.v
zip.v
| | Di
| 29.01.
| A
| Propositionale und Definitionale Gleichheit
| vl27.v
|
| Mi
| 30.01.
| H
| Abhängig getypte Programmierung in Coq und Agda
| coq-2008-01-30.v
agda-2008-01-30.v
| | Mo
| 04.02.
| Ü 14
| (Rosenmontag) Wiederholung
|
|
| Di
| 05.02.
| H 29
| (Faschingsdienstag) Klausur
|
| | Mi
| 06.02.
| H 30
| (Aschermittwoch) Besprechung der Klausur
|
|
Historischer Beweisbegriff, Mengentheorie als Formalisierung der Mathematik, Aufgaben und Verwendung
eines Beweispruefers (Theorembeweisers).
Nach oben.
Syntax und Semantik der Aussagenlogik.
Regeln des Gentzen'schen Sequenzenkalküls, Korrektheit und Vollstaendigkeit.
Nach oben.
Sequenzenkalkül, PVS
Material:
Nach oben.
- Klauseln und -generierung
- Resolutionsregel
- Korrektheit und Vollständigkeit
Nach oben.
- Disjunktionseigenschaft
- Brouwer-Heyting-Kolmogorov-Interpretation
- Natürliches Schliessen
- Beweisterme
Nach oben.
Vorstellung eines Algorithmus zur Klauselgenerierung; Resolution.
Konstruktive Beweise in Tutch.
Nach oben.
- Davis-Putnam Logemann-Loveland: Erfüllbarkeitsprozedur (SAT-Solver)
- Untypisierte Prädikatenlogik
- Typisierte Prädikatenlogik: Syntax (formal) und Semantik
Nach oben.
- Beispiele von Tautologien
- Sequenzenkalkül
- Korrektheit des Sequenzenkalküls
- Vollständigkeit des Sequenzenkalküls (Skizze)
Nach oben.
Verbesserung von Blatt 2. Beweis der Korrektheit des
Klauselgenerierungsalgorithmusses. zChaff Mini-Tutorial. FOL-Beweise in PVS.
Material:
Nach oben.
- Beweisreduktionen (β)
- Subject reduction (Erhaltung der Aussage under Reduktion)
- Normale Beweise für das Konjunktiv-Implikative Fragment
- Beweis der Normalisierung
Nach oben.
- Kripke-Modelle für konstruktive Aussagenlogik
- Widerlegung durch Gegenmodell
- Korrektheit des natürlichen Schließens
- Vollständigkeit des natürlichen Schließens
Nach oben.
- Konstruktiver Beweis = funktionales Programm.
- Beweisbaum = Typherleitung.
- Funktionen höherer Ordnung.
- β-Reduktion.
- Kripke-Gegenmodelle.
Nach oben.
- 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.
- Induktion in PVS: Listen
expand induct replace rewrite auto-rewrite ground grind induct-and-simplify>
- Datei: ue8/list.pvs
|
Andreas Abel
Last modified: Tue Dec 11 10:00:19 CET 2007
|
|
|