Logic and Computability (Out-Dated)
IMPORTANT INFORMATION
This website is out-dated!
You can find the current course information and materials at our teaching wiki.Out-Dated Information:
This lecture provides an introduction to different logics and their decidability.
- Propositional Logic: Motivation, Syntax, Semantics, Proof Rules, Complexity, CNF, ...
- Predicate-Logic: Syntax, Deduction, Semantics, Decidability, decidable theories, ...
In the practicals, tasks that fit the subjects taught in the lecture have to be solved.
News
Logic and Computability was awarded the Prize for Excellence in Teaching. Read more in the news section.
Course Language
The course is taught in English. Questions by students can also be asked in German.
Teaching Concept
A detailed statement about the didactic concepts employed in this course is available for download (as of winter semester 2013/14; German only).
Course Materials
Slides and other materials (if any) will be published here after each lecture. Some of the material is password-protected, for copyright reasons. If you are enrolled for the course, send an email to the lecturer if you need the password.
Date and Topic | Course Material |
---|---|
2014-10-07 Introduction, Motivation, Administrative Information |
Slides (PDF) |
2014-10-14 Syntax and Semantics of Propositional Logic |
Slides (PDF) Blackboard (ZIP) Online SUDOKU Solver |
2014-10-21 Natural Deduction for Propositional Logic |
Slides (PDF) Scanned Overhead Slide (PDF) Blackboard (ZIP) Download Deduction Rules (PDF) Pandora Proof Checker |
2013-10-28 Combinational Equivalence Checking, Normal Forms, Tseitin's Encoding |
Slides (PDF) Blackboard (ZIP) DIMACS File from Equivalence Check |
2014-11-04 SAT Solver, DPLL, Learning, Refutation Proofs |
Slides (PDF) Blackboard (ZIP) |
2014-11-11 Symbolic Encoding and Computations, Craig Interpolation |
Slides (PDF) Scanned Overhead-Slide (PDF) Blackboard (ZIP) |
2013-11-19 Binary Decision Diagrams |
Slides (PDF) Scanned Overhead-Slides (PDF) Blackboard (ZIP) Password-protected: Book chapter on BDDs by Hachtel & Somenzi (PDF) Password-protected: Handout - Summary of BDDs (PDF) |
2014-11-25 Predicate Logic: Syntax, Semantics, Models |
Slides (PDF) Blackboard (ZIP) |
2014-12-02 Natural Deduction for Predicate Logic |
Slides (PDF) Scanned Overhead Slide (PDF) Blackboard (ZIP) Password-protected: Pandora Lite (ZIP) |
2013-12-10 A Real Proof in Natural Deduction |
Slides (PDF) Blackboard (ZIP) Proof (exported from Pandora) |
2014-12-16 Theories in Predicate Logic and SMT |
Slides (PDF) Blackboard (ZIP) |
2015-01-13 Decidability and the Undecidability of Predicate Logic |
Slides (PDF) Blackboard (ZIP) |
2015-01-20 Relation to Current Research @IAIK |
Slides (PDF) |
Learning Targets
Here is a summary of all learning targets of the course, for winter term 2014/15.
Exams
In general, exams are done in writing. If less than four candidates are registered for a particular exam, the exam will be done orally. Dates for (written) exams are set in TUGrazonline; please register there. Oral exams can be done anytime. Contact the lecturer to make an appointment for an oral exam.
Exams consist of both theoretic questions and practical questions. Theoretic questions are, in principle, similar to the self-control questions posed at the end of each lecture; practical questions are, in principle, similar to the tasks given in the practicals' assignments. However, the complexity of the questions is scaled to make them adequate for the time available during an exam.
The questions at written exams are posted in English. Answers can be given either in English or in German, at the student's discretion. Furthermore, these rules apply to written exams.
Oral exams can be done either in English or in German, at the student's discretion. An oral exam will typically last approximately one hour.
Exams are usually preceeded by a Question Hour on the day before. For written exams, this will be announced as a comment in the exam registration in TUGRAZonline. For oral exams, please make an individual appointment. The purpose of the Question Hour is to clarify any issues you might have encountered while preparing for the exam.
The following sheet containing the proof rules of the natural deduction calculus may be used during an exam.
Copies will be distributed at the beginning of an exam.
Download Deduction Rules (PDF)
In case they are needed, a copy of McMillan's interpolation rules and of
Tseitin's encoding rules will also be distributed.
Other than that, no lecture notes, or any other materials are allowed during an exam.
Practicals
It is highly recommended to take the homonymous practical course in parallel to this lecture. The assignments of the practicals are tailored towards the content presented in the lecture. Surveys among students from previous years indicate that the effort required for studying for the lecture's exam is decreased significantly by taking part in the practicals.
Title: Logic and Computability
Course-Number: 705.033
Lecturer: Georg Hofferek
E-Mail: georg.hofferek@iaik.tugraz.at
Newsgroup: tu-graz.lv.logik
TUGRAZonline: TUGRAZonline
Twitter: @GeorgHofferek, #iaikLuB