Vorlesungs-Folien

H. Peter Gumm: Rechnergestützte Beweissysteme

0. Einleitung
   • Logik
   • Anwendungen in der Informatik
1. PVS
   • Das PVS System
   • Installation
     
   • Einfache Beweise
2. Aussagenlogik
   • Aufbau logischer Sprachen
   • Aussagenlogik
   • Hilbert Kalkül
     
   • Sequenzenkalkül
   • Resolventenkalkül
     
3. Prädikatenlogik
   • Formeln
   • Signaturen
   • Terme
   • Syntax
   • Spezifikationen
4. Kalküle der Prädikatenlogik
   • Sequenzenkalkül
   • Skolemisieren und Instanziieren
   • Korrektheit, Vollständigkeit
   • Behandlung der Gleichheit
   • Resolventenmethode der Prädikatenlogik
5. Typen und Typinferenz
   • Kontexte
   • Typkonstruktionen
   • Typüberprüfung
6. Induktion
   • Nichtstandardmodelle
   • Induktion in PVS
   • Freiheitsaxiome
   • Induktive Datentypen
     
7. Abstrakte Datentypen
   • DATATYPE in PVS
   • Axiome
   • Pattern und CASES
8. Entscheidungsverfahren
   • Entscheidungsprobleme
   • Arithmetik
   • Solver
   • Fourier-Motzkin
   • Kongruenzabschluss
   • Knuth-Bendix
   • Nelson-Oppen
     
9. Logik höherer Stufe
• Syntax
• Lambda-Kalkül
• Inferenzregeln
• Dependent Types
10. Typsysteme
• Polymorphes Typsystem
• Terme
• Binder
• Beweis: Cantor in PVS
11. Intuitionistische Logik
    
• Regeln
• Tertium Non Datur
  
• Heyting-Semantik
• Vollständigkeit
  
12. Jape
• Benutzung von JAPE
• Theorie Funktionaler Programme
  
• Implementierung eigener Logiken
  
13. Das Lambda-System
    
• Hardware aus Beweisen
• Regeln
• Beispiel