Formale Systeme - i12 · Organisatorisches Ubungen¨ I Große Ubungen alle zwei Wochen freitags;¨...
29
KIT – I NSTITUT F ¨ UR THEORETISCHE I NFORMATIK Formale Systeme Organisatorisches Prof. Dr. Peter H. Schmitt KIT – Universit¨ at des Landes Baden-W ¨ urttemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft www.kit.edu
Transcript of Formale Systeme - i12 · Organisatorisches Ubungen¨ I Große Ubungen alle zwei Wochen freitags;¨...
KIT – INSTITUT FUR THEORETISCHE INFORMATIK
Formale SystemeOrganisatorischesProf. Dr. Peter H. Schmitt
KIT – Universitat des Landes Baden-Wurttemberg undnationales Forschungszentrum in der Helmholtz-Gemeinschaft
www.kit.edu
Organisatorisches
Ubungen
I Große Ubungen alle zwei Wochen freitags;erstmals am 28.10.11
I Ubungsblatter jeweils montags;erstes Blatt am Montag, dem 24.10.11
Zwischenklausuren und Praxisaufgaben
I Eine ZwischenklausurI Zwei PraxisaufgabenI Die Teilnahme ist freiwilligI Die erzielten Punkte werden als Bonuspunkte auf die
bestandene Abschlussklausur angerechnet
Prof. Dr. Peter H. Schmitt – Formale Systeme 2/9
Organisatorisches
Ubungen
I Große Ubungen alle zwei Wochen freitags;erstmals am 28.10.11
I Ubungsblatter jeweils montags;erstes Blatt am Montag, dem 24.10.11
Zwischenklausuren und Praxisaufgaben
I Eine ZwischenklausurI Zwei PraxisaufgabenI Die Teilnahme ist freiwilligI Die erzielten Punkte werden als Bonuspunkte auf die
bestandene Abschlussklausur angerechnet
Prof. Dr. Peter H. Schmitt – Formale Systeme 2/9
Organisatorisches
Ubungen
I Große Ubungen alle zwei Wochen freitags;erstmals am 28.10.11
I Ubungsblatter jeweils montags;erstes Blatt am Montag, dem 24.10.11
Zwischenklausuren und Praxisaufgaben
I Eine ZwischenklausurI Zwei PraxisaufgabenI Die Teilnahme ist freiwilligI Die erzielten Punkte werden als Bonuspunkte auf die
bestandene Abschlussklausur angerechnet
Prof. Dr. Peter H. Schmitt – Formale Systeme 2/9
Organisatorisches
Ubungen
I Große Ubungen alle zwei Wochen freitags;erstmals am 28.10.11
I Ubungsblatter jeweils montags;erstes Blatt am Montag, dem 24.10.11
Zwischenklausuren und Praxisaufgaben
I Eine ZwischenklausurI Zwei PraxisaufgabenI Die Teilnahme ist freiwilligI Die erzielten Punkte werden als Bonuspunkte auf die
bestandene Abschlussklausur angerechnet
Prof. Dr. Peter H. Schmitt – Formale Systeme 2/9
Praxisaufgaben
Praxisaufgaben machen mit konkreten Systemen vertraut
I minisatEin System zu Erfullbarkeitsprufung aussagenlogischerFormeln (SAT Solver).
I KeYEin interaktives Beweissystem fur Pradikatenlogik ersterStufe
Prof. Dr. Peter H. Schmitt – Formale Systeme 3/9
Praxisaufgaben
Praxisaufgaben machen mit konkreten Systemen vertraut
I minisatEin System zu Erfullbarkeitsprufung aussagenlogischerFormeln (SAT Solver).
I KeYEin interaktives Beweissystem fur Pradikatenlogik ersterStufe
Prof. Dr. Peter H. Schmitt – Formale Systeme 3/9
Webseite
Webseite zur Vorlesung
http://i12www.ira.uka.de/˜pschmitt/FormSys/FormSys1112/
Enthalt alle fur die Vorlesung relevanten Informationen undMaterialien:
I VorlesungsskriptumI FolienI UbungsblatterI Termine
Prof. Dr. Peter H. Schmitt – Formale Systeme 4/9
Webseite
Webseite zur Vorlesung
http://i12www.ira.uka.de/˜pschmitt/FormSys/FormSys1112/
Enthalt alle fur die Vorlesung relevanten Informationen undMaterialien:
I VorlesungsskriptumI FolienI UbungsblatterI Termine
Prof. Dr. Peter H. Schmitt – Formale Systeme 4/9
Klausuren
Klausurtest
Freitag, 13.01.2012, 11:30 Uhr
1. Klausurtermin
Dienstag, 14.02.12, 14:00 Uhr
2. Klausurtermin
Donnerstag, 12.04.2012, 14:00 Uhr
Prof. Dr. Peter H. Schmitt – Formale Systeme 5/9
Forum
Unter der Adresse
http://i12www.ira.uka.de/ farago/fsforum
haben wir ein Forum zur Vorlesung eingerichtet.
Dort konnen Sie Fragen und Antworten zum Inhalt, zurOrganisation, zu Prufungen, ... einstellen.
Wir werden das Forum regelmaßig lesen.
Prof. Dr. Peter H. Schmitt – Formale Systeme 6/9
Forum
Unter der Adresse
http://i12www.ira.uka.de/ farago/fsforum
haben wir ein Forum zur Vorlesung eingerichtet.
Dort konnen Sie Fragen und Antworten zum Inhalt, zurOrganisation, zu Prufungen, ... einstellen.
Wir werden das Forum regelmaßig lesen.
Prof. Dr. Peter H. Schmitt – Formale Systeme 6/9
Forum
Unter der Adresse
http://i12www.ira.uka.de/ farago/fsforum
haben wir ein Forum zur Vorlesung eingerichtet.
Dort konnen Sie Fragen und Antworten zum Inhalt, zurOrganisation, zu Prufungen, ... einstellen.
Wir werden das Forum regelmaßig lesen.
Prof. Dr. Peter H. Schmitt – Formale Systeme 6/9
InhaltsubersichtI Aussagenlogik: Syntax und Semantik
I Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: Kalkule
I Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: Anwendungen
I Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und Semantik
I Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: Kalkule
I Pradikatenlogik: AnwendungenPeano Arithmetik Neu
I GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik Neu
I GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI Gleichheit
I JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) Neu
I Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale Aussagenlogik
I Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)
I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)
I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi Automaten
I Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
InhaltsubersichtI Aussagenlogik: Syntax und SemantikI Aussagenlogik: KalkuleI Aussagenlogik: AnwendungenI Pradikatenlogik: Syntax und SemantikI Pradikatenlogik: KalkuleI Pradikatenlogik: Anwendungen
Peano Arithmetik NeuI GleichheitI JML (Java Modeling Language) NeuI Modale AussagenlogikI Temporale Logik (LTL)I Endliche Automaten (Wiederholung)I Buchi AutomatenI Modellprufung
Prof. Dr. Peter H. Schmitt – Formale Systeme 7/9
Literatur
PETER H. SCHMITT: Formale Systeme. Skriptum zurVorlesung.
MELVIN FITTING: First Order Logic and Automated TheoremProving.
U. SCHONING: Logik fur Informatiker.V. SPERSCHNEIDER/G. ANTONIOU: Logic: a Foundation for
Computer Science.ALONZO CHURCH: Introduction to Mathematical Logic.EBBINGHAUS/FLUM/THOMAS: Mathematische Logik.LOVELAND: Automated Theorem Proving: a Logical Basis.SALLY POPKORN: First Steps in Modal Logic.M. R. HUTH AND M. D. RYAN: Logic in Computer Science.
Modelling and reasoning about systems.
Prof. Dr. Peter H. Schmitt – Formale Systeme 8/9
Literatur
PETER H. SCHMITT: Formale Systeme. Skriptum zurVorlesung.
MELVIN FITTING: First Order Logic and Automated TheoremProving.
U. SCHONING: Logik fur Informatiker.V. SPERSCHNEIDER/G. ANTONIOU: Logic: a Foundation for
Computer Science.ALONZO CHURCH: Introduction to Mathematical Logic.EBBINGHAUS/FLUM/THOMAS: Mathematische Logik.LOVELAND: Automated Theorem Proving: a Logical Basis.SALLY POPKORN: First Steps in Modal Logic.M. R. HUTH AND M. D. RYAN: Logic in Computer Science.
Modelling and reasoning about systems.
Prof. Dr. Peter H. Schmitt – Formale Systeme 8/9
Literatur
J. E. HOPCROFT AND J. D. ULLMANN: Introduction toAutomata Theory.
JAN VAN LEEUWEN (ED.): Handbook of Theoretical ComputerScience. Vol. B : Formal Models and Semantics.
Prof. Dr. Peter H. Schmitt – Formale Systeme 9/9
