Class sessions: Tuesdays 11:15 – 12:30 and Thursdays 9:45 – 11:00, East Hall 8
Topics: Formal languages, discrete automata, first-order logic. This course gives an introduction to the most basic themes of theoretical computer science. Formal languages and discrete automata are the fundaments of programming languages and their parsing and compiling. First-order logic is the basis of artificial intelligence, program verification and advanced data base systems.
Lecture notes: self-contained, complete set of lecture notes.
Further helpful documents:
The final exam from 2010 with solutions (multiple choice format) (pdf)
Additional reading: a condensed intro to RDF, written by Jan Wilken Dörrie. To be enjoyed at the end of the lecture as this concerns a marriage between logic and grammars, of central importance for "semantic web" techologies.
Course culture. The online lecture notes are a fully self-contained, textbook-style, detailed text. Any exam questions are based solely on what is in the lecture notes. Thus, a student could perfectly pass this course by just home-studying the lecture notes, tuning his/her skills on the weekly homeworks, sit in the exams, and be done without ever seeing me. Ooops. I do want to see my students... Easy: I make classroom attendance mandatory. Ooops again - mandatory boredom? Solution: (i) mandatory classroom presence, (ii) mandatory pre-reading of the lecture note portion of the day, (iii) in class I will only briefly rehearse the pre-read lecture note material, making sure that everybody has a good grasp of it, and then (iv) I will spend most of the classroom time telling you stuff that is related to the lecture note material, but outside of it -- stuff you will not find in typical lecture notes: historical background, applications, connections of computer science to other sciences, tricky problems and open questions, math minitutorials, and more. This "extra" stuff will, I hope, make attendance worth its while, although it is not exam-relevant. You will, I hope very much, be amazed how deeply the technical material of this lecture is connected to realities outside CS.
Grading and exams: Grading and exams: The final course grade will be composed from homeworks (10%), presence sheets (10%), active participation in class (5%), and quizzes/exams. There will be four miniquizzes (written in class, 20 minutes), the best three of which will each account to 15% of the final grade (worst will be dropped), and one final exam, counting 30%. All quizzes are open book. Each quiz or exam yields a maximum of 100 points. The total semester points Pts_total are computed as the weighted semester point average (each quiz points are weighted by 0.15, the final by 0.30, etc.), and from Pts_total the final grade is computed by the standard Jacobs formula.
Miniquiz makeup rules: if a miniquiz is missed without excuse, it will be graded with 0 points. An oral makeup will be offered for medically excused miniquizzes according to the Jacobs rules (especially, the medical excuse must be announced to me on the day of the miniquiz). Non-medical excuses can be accepted and miniquiz makeups be arranged on a case-by-case basis.
References (optional! the online lecture notes suffice)
Schoening, Uwe: Logic for Computer Scientists (Progress in Computer Science and Applied Logic, Vol 8), (Birkhauser). The book contains what its title suggests. IRC: QA9 .S363 1989
Schedule (this will be filled in synchrony with reality as we go along)
|Sep 3||Alphabets, languages, sizes of sets and languages.|
|Sep 8||Sizes of sets of languages. DFAs. Reading for Sep 8: Lecture Notes Section 2 and Section 3 up to Example 3.2 Exercise sheet 1|
|Sep 10||NFAs. Power set construction. Application: text search algorithm. Epsilon-NFAs. Reading: LN Section 3.1 complete.|
|Sep 15||Regular expressions and equivalence to DFAs. Reading: LN Section 3.2. Solutions to sheet 1 Exercise sheet 2|
|Sep 17||Algebraic laws for regexps. Pumping lemma. Reading: LN Sections 3.3, 3.4|
|Sep 22||(no class)|
|Sep 24||Miniquiz 1 (CS lecture hall, Res. 1) closure properties of regular languages Solutions to sheet 2 Exercise sheet 3|
|Sep 29||Myhill-Nerode theorem and minimization of DFAs. Reading: Section 3.6 Solutions to sheet 3 Exercise sheet 4|
|Oct 1||Context-free languages: basic definitions and examples. Ambiguity. Reading: Sections 4.1, 4.2|
|Oct 6||Grammars of regular languages. XML and friends. Reading: Sections 4.3, 4.4 Solutions the sheet 4 Exercise sheet 5|
|Oct 8||Pushdown automata. Reading: Section 4.5|
|Oct 13||Chomsky Normal Form. Reading: Section 4.6 Solutions to sheet 5 Exercise sheet 6|
|Oct 15||Miniquiz 2 (CS lecture hall, Res. 1) The CYK algorithm. Some (non)decidability results. No Reading.|
|Oct 22||Wrap-up formal languages. No reading, no exercises! Solutions to sheet 6|
|Oct 27||Introducing first-order logic. Term syntax. Reading: LN Section 6, Section 7 up to (including) Example 7.2 Exercise sheet 7|
|Oct 29||Syntax of FOL. Formalizing pieces of reality in FOL. Reading: LN Section 7.1.|
|Nov 3||Semantics of FOL: S-structures, S-interpretations. Reading: LN Section 7.2 up to Def. 7.7. Solutions to sheet 7 Exercise sheet 8|
|Nov 5||Miniquiz 3 (CS lecture hall, Res. 1) The model relationship. No reading|
|Nov 10||Exercise session: describing pieces of the world by FOL propositions. Exercise sheet 9|
|Nov 12||The model relationship, continued. Logical entailment. Reading: LN Section 7 to end.|
|Nov 17||A sequent calculus. Reading: LN Section 8 up to and including the overview table on page 85. Solutions to sheet 9 Exercise sheet 10|
|Nov 19||Derived rules and derivations. Reading: LN Section 8 complete.|
|Nov 24||Soundness and completeness of FOL. Reading: LN Section 9 up to the (*) statement after proposition 9.4 Solutions to sheet 10|
|Nov 26||Miniquiz 4 (CS lecture hall, Res. 1) Wrap-up session|
|Dec 1||(optional, only for the ones interested in more, and more practically applied, logic): Herbrand theory and a resolution calculus, part 1|
|Dec 3||(optional) Herbrand theory and a resolution calculus, finish|
|Dec 11||Final exam: 12:30-14:30, CS lecture hall|