Dr. Bernd Baumgarten   Fraunhofer - SIT  Rheinstr. 75  D-64295 Darmstadt  Germany

Tel (+49 or 0) 6151 - 869 263                           Fax (+49 or 0) 6151 - 869 224  E-mail bernd.baumgarten at-symbol sit.fraunhofer.de

Working for Fraunhofer

·  Fraunhofer-Gesellschaft

·  Fraunhofer Institute for Secure Information Technology SIT

Teaching

·  Logik SS 2012
·  Former Courses of Mine

Yours Truly

·  My Research Interests + Publications
·  My Hobbies

                                                                                                                                                                          

Vorlesung Logik SS 2012 an der h_da, [Hochschule|University of Applied Sciences] Darmstadt

(W. Shakespeare)

Inhalt
Logiken: Aussagenlogik, Prädikatenlogik (1. Stufe), andere Logiken (modale, temporale, Beschreibungs-Logik)
jeweils:   Syntax, Semantik, wichtige Begriffe und Sätze, Algorithmen und Kalküle, Anwendung

Skript (entspricht den Folien):
Mathematische Grundlagen - Aussagenlogik - Prädikatenlogik - AndereLogiken - Literatur, Inhalt

Folien:
   Mathematische Grundlagen  A
   Aussagenlogik  B C D E 
   Prädikatenlogik  F G
   Andere Logiken

Übungsaufgaben  1-53
Zusatzübungen AL
Gelöste Aufgaben (Achtung ...) 1-25  26-31

Literatur
Jürgen Dassow: Logik für Informatiker, Teubner, 2005
Martin Kreuzer, Stefan Kühling: Logik für Informatiker, Pearson Studium, 2006
Uwe Schöning: Logik für Informatiker, 5. Aufl., Spektrum, 2000/05
Franz Baader et al., Hrsg.: The Description Logic Handbook, Cambridge University Press, 2003

Zeit/Ort
ab 20.03.12  -  Mo., 08.30 Uhr  / Di., 08:30 Uhr  -  jetzt: D14, Raum 104

Stoff pro Block
20.03.12:  Math. Grundlagen - Mengen, Relationen, Funktionen
26.03.12:  Übungen. Induktion, Rekursion, Grammatiken
27.03.12:  Aussagenlogik - Syntax, semantische Grundlagen, Junktoren, Modelle, Tautologien u.a. spezielle Formeltypen, Anwendungen
02.04.12:  Übungen
03.04.12:  Substitution und Ersetzung, Junktorenbasen, Folgerungen, Theorien
16.04.12:  Übungen.
17.04.12:  Folgerungen, Theorien (Rest), Konjunktive Normalform, AL-Resolution
23.04.12:  Übungen, Disjunktive Normalform, AL-Tableaux
24.04.12:  weiter: DNF, AL-Tableaux, SAT, PROLOG-Grundideen, Binary Decision Diagrams
30.04.12:  AL-Axiome und -Kalküle, insbes. "Werkzeugkasten"
07.05.12:  Übungen, Interpolations- und Kompaktheitssätze
08.05.12:  Prädikatenlogik - Einführung und Syntax
14.05.12:  Übungen, PL Semantik: Strukturen, Interpretationen
15.05.12:  Interpretationen, Auswertung von Termen und Formeln, Semantische Begriffe,
                 wichtige Äquivalenzen und Tautologien, Feinheiten der Substitution, "frei für"
geplant
21.05.12:  Übungen
22.05.12:  Halbentscheidbares und Unentscheidbares, Axiomatische PL1-Kalküle, PL1-Tableaux
04.06.12:  Übungen, PL1-Werkzeugkasten
05.06.12:  Normalformen (PNF, Skolem, Klausel-NF), Erfüllbarkeitsäquvalenz
11.+12.06.12:  fällt aus
18.06.12:  Übungen,
19.06.12:  PL1-Resolution, Andere Logiken - Modale Logik 1
25.06.12:  Übungen, Modale Logik 2
26.06.12:  Temporale Logik 1, Buechi-Automaten
02.07.12:  Übungen und Temporale Logik 2
03.07.12:  restl. Aufgaben ML & PLTL, Zusatzaufgaben
09.07.12:  Zusatzaufgaben (Rest)
10.07.12:  Wiederholung und offene Fragen
Klausur

                                                                                                                                                                          

Former Courses

1. Vorlesung Theoretische Informatik WS 2011/12 an der h_da, [Hochschule|University of Applied Sciences] Darmstadt

Folien:              ... basieren auf den Folien von Herrn Lange; eventuelle Fehler gehen auf meine Kappe
Folien 0.1 - 07.10.2011  Folien 0.2 - 14.10.2011
Folien 1.1 - 14.10.2011  Folien 1.2 - 14.10.2011  Folien 1.3 - 25.10.2011
Folien 2.1 - 14.11.2011  Folien 2.2 - 14.11.2011  Folien 2.3 - 16.11.2011
Folien 2.4 - 29.11.2011  Folien 2.5 - 18.11.2011  Folien 2.6 - 05.12.2011
Folien 3.1 - 15.12.2011  Folien 3.2 - 23.12.2011  Folien 3.3 - 23.12.2011
Folien 3.4 - 25.12.2011

Übungsblätter: ... basieren auf denen von Herrn Lange; dito.
Übungsblatt 1  Übungsblatt 2  Übungsblatt 3  Übungsblatt 4
Übungsblatt 5  Übungsblatt 6 (s.u.) Übungsblatt 7
Zusatzaufgaben

Weitere Materialien:
Pumping-Lemma, ausführliche Hinführung
Logische Aspekte des Pumping-Lemmas
Umformungen zwischen den Arten, reguläre Sprachen zu definieren
CYK Animation
Ein Kellerautomat für Klammerungen
Vorlesungsextrakt (darf bei mir in der Klausur Feb. 2012 verwendet werden)
Notizen zu Übungsblatt 6 Aufgabe 3

Inhalte:
Organisatorisches, Motivation, Einordnung (mit Beispielen zur Komplexitäts- und Berechenbarkeitstheorie)
Grundbegriffe  Sprachen, Mengen, Relationen, Graphen, Wege
Endliche Automaten Grundlagen, Minimierung, Stringmatching
Formale Sprachen Chomsky-Grammatiken Reguläre Sprachen Reguläre Grammatiken, Nichtdeterministische Automaten, Abgeschlossenheitseigenschaften,
Pumping-Lemma, Reguläre Ausdrücke
Kontextfreie Sprachen Grundlagen, CYK-Algorithmus, Chomsky-Normalform, Kellerautomaten
Berechnungstheorie: Grundlagen, RAM, Turing-Maschinen, Churchsche These, Algorithmisch unlösbare
Probleme, Satz von Rice

                                                                                                                                                                          

2. Vorlesung Petrinetze WS 2008/09 an der h_da, Hochschule Darmstadt

Zeit: Di., 08.30 Uhr
Ort: Informatik, Raum 303
Stoff:
Spezifikationen und formale Sprachen, Induktion und Rekursion
Akzeptoren (Automaten), kanonischer Akzeptor einer Sprache, Grammatiken,
reguläre Ausdrücke, kommunizierende Automaten, Netzgraphen, ST-Systeme
Netzdynamik, Netzsprachen, Übungen
Netzsprachen weiter, Lebendigkeit, Analyse-Ziele, Übungen
Erreichbarkeitsanalyse + Übungen, Überdeckungsanalyse
Überdeckungsanalyse + Übungen, Lineare Analyse
Analyse-Übungen, Nebenläufigkeitsaspekte, High Level Petri Nets (HLPN)
HLPNs: Anwendung und Übungsaufgaben (1)
HLPNs (2), Netze mit quantitativer Zeit (1)
Netze mit quantitativer Zeit (2), Übungsaufgaben zur Wiederholung
Übungsaufgaben zur Wiederholung

Skript
Seiten 1 bis 8
Seiten 9 bis 16
Seiten 17 bis 24
Seiten 25 bis 30

Lösungen der Modellaufgaben Vorsicht!
1: Induktive Mengen- und rekursive Funktionsdefinitionen
2: Kanonischer Akzeptor und reguläre Ausdrücke
3: Netzsprachen
4: Netzsprachen
5: Grammatiken, Ziel-Netzsprachen
6: Erreichbarkeitsanalyse
7: Erreichbarkeitsanalyse, Erreichbarkeitsanalysegraph
8: ST-System für einen Erreichbarkeitsgraphen vorgegebener Form
9: Überdeckungsanalyse
10: Überdeckungsanalyse
11: Netze mit individuellen Marken (HLPN)
12: Netze mit individuellen Marken (HLPN) und Faltung
13: Systemmodellierung mit HLPN
14: Timernetze

Worum geht es bei den Petrinetzen?

Petrinetze sind ein formales Beschreibungsmittel (FBM) für das Verhalten verteilter
Systeme. Sie verallgemeinern auf naheliegende Weise die endlichen Automaten.

Mit FBMs allgemein kann man Systeme (in gewissem Sinne) mathematisch genau
spezifizieren. Mit einer formalen Spezifikation kann man in vielen Fällen ...

• alle möglichen Verhaltensweisen eines spezifikationsgemäßen Systems untersuchen,
• prüfen, ob ein spezifikationsgemäßes System gewünschte Dinge tun oder unerwünschte unterlassen wird,
• prüfen, ob eine Implementierung (mit formaler Semantik) die Spezifikation erfüllt,
• rasch eine evtl. langsame Implementierung erzeugen (rapid prototyping),
  
• Testfälle für Implementierungen automatisch generieren,
• schon beim Hinschreiben Fehler in der informellen Spezifikation finden.
  

Viele Analysemethoden für die obigen Aufgaben existieren in jeweils angepasster Form für
fast alle FBMs. Petrinetze zeichnen sich aber vor anderen FBMs durch ihre anschauliche
Verständlichkeit und spezielle - nur bei ihnen funktionierende - Analysemöglichkeiten aus.

In der Vorlesung arbeiten wir mit vielen praktischen Beispielen, auch solchen außerhalb der
Datenverarbeitung.

                                                                                                                                                                            

3. Course Formal Methods  WS 2007/08 at h_da, University of Applied Sciences Darmstadt

Achtung: Aus mir nicht ganz klaren Gründen hielten wir die Vorlesung auf Deutsch
but with English slides and lecture notes.
Aber wir sind ja auch Dinge wie Back-Shops gewohnt ... (Gegenteil: Front-Shop?)
Als Hilfestellung für die Hörer gab es ein partielles einschlägiges Vokabelverzeichnis.

My part of the course covered
Petri Nets and Abstract Data Types.
Mathematical preliminaries, languages, canonical automaton of a language
Languages continued, PT systems
PT systems continued; Analysis introduction
Net languages: target markings, exercises.
Analysis of PT systems: Boundedness, Reachability analysis (2 Exercises), Coverability analysis (Part 1)
Part 2+Exercise Coverability analysis, Linear analysis
High Level Petri Nets (HLPNs)
Abstract data types (ADT) overview
Data objects, data types, abstraction
Single-/many-sorted algebras and signatures, isomorphisms,
Congruences, quotients. Assignment, evaluation, substitution. Consequences of axioms
Junk, confusion, and initiality.What is specified by an ADT spec?
ADT Practicalities and extensions. PN and ADT review exercises.

Course Notes
PN+ADT notes
Model Exercises for Petri Nets
Model Exercises for ADTs
Additional Exercises
Languages and PT Systems, Abstract Data Types
Additional Petri net exercises in German can be found here.
Additional Help
1. Two people asked about additional exercise #9(b).
    I thought it might be in order here to review a few ADT notions and give some hints.
2. Some people use programming language assignments in transiton conditions of HLPNs.
    Don't! Here is why.

                                                                                                                                                                           

4. Druskininkai Lectures (May 2007)

Corrected + supplemented version of slides:

• Formal specification, observability, discreteness, and languages
• Abstract Data Types
• Petri Net basics
• High level Petri Nets 1
• High level Petri Nets 2
• Petri Nets with timing notions

                                                                                                                                                                           

If you care to know: I am also interested in ...

• Dancing (now Swing, i.e. Lindy Hop, East Coast, Charleston, Balboa, Shag;

                        formerly Standard and Latin ballroom, Line dance) 

• Languages (natural ones, not only the formal ones of Theoretical Computer Science)
• History (once my weakest subject in school, and in spite of Nietzsche's warnings in

                       "Vom Nutzen und Nachtheil der Historie für das Leben")

• Logic (beyond the lecture above)
• Aikido (THE - now former - hobby of mine for 25 years)
• Playing Music (now Piano, formerly Guitar)
• how to find the time necessary to pursue these and other interests.

Are you interested in any of  these topics?
I've got a (pretty neglected) private homepage dealing with some of them.
Topics partially covered by now:
- Line dancing
- Logic
- Swing dancing

Last Change: May 15, 2012