Material
Material zur Vorlesung "Automatisierte Logik und Programmierung"
Vollständiges Skriptum pdf ps
Einzelne Kapitel
| Kapitel 1 |
Einführung | ps | |
| Kapitel 2 |
Formalisierung von Logik, Berechenbarkeit und Typdisziplin |
ps | |
| Kapitel 3 |
Die Intuitionistische Typentheorie |
ps | |
| Kapitel 4 |
Automatisierung des formalen Schliessens |
ps | |
| Kapitel 5 |
Automatisierte Softwareentwicklung |
ps | |
| Anhang A |
Typentheorie: Syntax, Semantik, Inferenzregeln |
ps | |
| Anhang B |
Konservative Erweiterungen der Typentheorie und ihre Gesetze |
ps | |
| Literatur- verzeichnis |
ps |
Artikel
- Kreitz: "Derivation of a Fast Integer Square Root Algorithm" pdf ps
- Constable, Kreitz: "Formal Derivation of an Algorithm for the Stamps Problem" pdf ps
The Nuprl Proof Development System, Version 5:
Reference Manual and User's Guide pdf ps
Individual Chapters
| Chapter 1 |
Introduction |
ps | |
| Chapter 2 |
A quick overview |
ps | |
| Chapter 3 |
Running Nuprl |
ps | |
| Chapter 4 |
The Navigator and the Top Loops |
ps | |
| Chapter 5 |
Editing Terms |
ps | |
| Chapter 6 |
Interactive Proof Development |
ps | |
| Chapter 7 |
Definition and Presentation of Terms |
ps | |
| Chapter 8 |
Rules and Tactics |
ps | |
| Appendix A |
The Basic Nuprl Type Theory |
ps | |
| Appendix B |
Introduction to Nuprl ML |
ps |
