Rechnergestütztes Beweisen

Zeitplan

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  


Vorlesung Hofmann 1: Einführung

Historischer Beweisbegriff, Mengentheorie als Formalisierung der Mathematik, Aufgaben und Verwendung eines Beweispruefers (Theorembeweisers).

Nach oben.


Vorlesung Hofmann 2: Sequenzenkalkül

Syntax und Semantik der Aussagenlogik. Regeln des Gentzen'schen Sequenzenkalküls, Korrektheit und Vollstaendigkeit.

Nach oben.


Übung 1

Sequenzenkalkül, PVS

Material:

Nach oben.


Vorlesung Hofmann 3: Resolution

  • Klauseln und -generierung
  • Resolutionsregel
  • Korrektheit und Vollständigkeit

Nach oben.


Vorlesung Abel 1: Einführung in die Konstruktive Logik

  • Disjunktionseigenschaft
  • Brouwer-Heyting-Kolmogorov-Interpretation
  • Natürliches Schliessen
  • Beweisterme

Nach oben.


Übung 2

Vorstellung eines Algorithmus zur Klauselgenerierung; Resolution. Konstruktive Beweise in Tutch. Nach oben.


Vorlesung Hofmann 4: DPLL, Prädikatenlogik

  • Davis-Putnam Logemann-Loveland: Erfüllbarkeitsprozedur (SAT-Solver)
  • Untypisierte Prädikatenlogik
  • Typisierte Prädikatenlogik: Syntax (formal) und Semantik

Nach oben.


Vorlesung Hofmann 5: Prädikatenlogik: Sequenzenkalkül, Korrektheit

  • Beispiele von Tautologien
  • Sequenzenkalkül
  • Korrektheit des Sequenzenkalküls
  • Vollständigkeit des Sequenzenkalküls (Skizze)

Nach oben.


Übung 3

Verbesserung von Blatt 2. Beweis der Korrektheit des Klauselgenerierungsalgorithmusses. zChaff Mini-Tutorial. FOL-Beweise in PVS.

Material:

Nach oben.


Vorlesung Abel 2: Beweisnormalisierung

  • Beweisreduktionen (β)
  • Subject reduction (Erhaltung der Aussage under Reduktion)
  • Normale Beweise für das Konjunktiv-Implikative Fragment
  • Beweis der Normalisierung

Nach oben.


Vorlesung Abel 3: Kripke-Modelle

  • Kripke-Modelle für konstruktive Aussagenlogik
  • Widerlegung durch Gegenmodell
  • Korrektheit des natürlichen Schließens
  • Vollständigkeit des natürlichen Schließens

Nach oben.


Übung 4: Konstruktive Logik: Normalisierung und Gegenmodelle

  • Konstruktiver Beweis = funktionales Programm.
  • Beweisbaum = Typherleitung.
  • Funktionen höherer Ordnung.
  • β-Reduktion.
  • Kripke-Gegenmodelle.
Nach oben.


Vorlesung Hofmann 6: Prädikatenlogik - Sequenzenkalkül

  • Vollständigkeit des Sequenzenkalküls

Nach oben.


Vorlesung Hofmann 7: Satz von Herbrand, Unifikation, Resolution

  • Satz von Herbrand
  • Unifikation für Terme erster Stufe
  • Resolution für Logik erster Stufe
  • Pränex-Form

Nach oben.


Vorlesung Hofmann 8: Kompaktheitssatz, Gleichheit

  • 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.


Übung 8

  • Induktion in PVS: Listen
  • expand induct replace rewrite auto-rewrite ground grind induct-and-simplify>
  • Datei: ue8/list.pvs
Valid HTML 4.01!
Andreas Abel
Last modified: Tue Dec 11 10:00:19 CET 2007
Valid CSS!