# Logic 2017 (English)

If you are taking the “Logik” lecture as part of the “Theoretical Computer Science Amendment” (see Module 89-5021), please contact Peter Zeller as early as possible. We will provide more information on request.

## Exercise Sheets

- Exercise 1
- Exercise 2 (Deadline: April 28th)
- Exercise 3
- Exercise 4 (Deadline: May 12th)
- Additional material: F0 proofs in Isabelle

- Exercise 5
- Exercise 6 (Deadline: May 26th)
- Additional material: tableaux_java2.zip
- Solution for exercise 4

- Exercise 7 (update 26.05: Fixed typo in 3b: semantic equivalence instead of syntactic equivalence)
- Exercise 8 (Deadline: June 9th)
- Exercise 9
- Exercise 10 (Deadline: June 23rd)
- Midterm exam
- Exercise 11
- Exercise 12 (Deadline: July 7th)
- Exercise 13
- Exercise 14 (Deadline: July 17th)

## Material

- An English translation of the slides from 2014 is available. Thanks to Erik Steiner for the translation!
- You can find the syllabus of the “Theoretic Computer Science Amendment”-version of Logic in the Modulhandbuch, Module 89-5021. Note that Gentzen sequent calculus for propositional logic and the Tableaux method in predicate method are not included in the syllabus. (The Tableaux method for propositional logic is included!)

If you want additional information or a different presentation of the contents of the lecture, you may find these links useful:

- The
**Davis-Putnam algorithm**is described here (Slides 1 to 8) and here. Note that we use the rules pure, unit, subsumption reduce, and splitting. You have to use them in this order, as is defined in pseudo code on our Slide 120. The examples on Slides 117 and 118 of our lecture will be helpful. There is quite some material on the web, search for Davis-Putnam or DPLL algorithm. **Resolution**is explained here (Slides 1 to 6 on Page 1) and here. Please also check the examples on our Slides 125 to 127. Alternatively, you can google for resolution rule and propositional logic.- The
**tableau method**is described here and here (we decompose conjunctions). Also check the examples on our Slides 77, 87 to 90. Again, Google may provide more information. - Our
**system F0**is precisely what is described in Gaifman’s notes. Up to the third axiom, it coincides with system H2 that Anita Wasilewska discusses in Chapter 8 (starting from Page 10) and Chapter 9 of her book. - The
**sequent calculus**is introduced (in slightly different notation) under the name Gentzen Style Proof System in Anita Wasilewska’s Chapter 11. - A
**good overview**of topics on predicate logics can be found here. - An
**introduction to predicate logic**together with a description of**Herbrand theory**,**unification**, and**resolution**can be found in this course on artificial intelligence. Concerning the syntax of predicate logic, you may prefer to use our notation on Slides 144 to 147 (syntax) and 155 to 158 (semantics). - The
**tableaux method**for predicate logic is explained in these notes. - A proof of
**undecidability of validity**via a reduction of PCP can be found here. You may compare the development with Slides 190 to 194. **Quantifier elimination**in QBF is described here (cf. Slides 171 and 172).- Gödel’s
**System F**is explained in Enderton’s book as well as Slides 199 to 212. **First-order theories**are introduced here, the relationship between axiomatizability and decidability is discussed here. More information is given on Slides 213 to 225.- Lecture notes in
**English**by Haim Gaifman can be found here. - This course by Anita Wasilewska comes with slides as well as lecture notes in
**English**.

## Prerequisite

To be admitted to the final exam, you need to solve the exercise sheets and achieve 50% of the overall points.

Every second sheet is designed to be solved in the exercise session (“Bearbeitung in der Übung”). Since the exercise sessions are in German you don’t have to attend them, but we recommend you to solve and hand-in the respective sheets. For the overall points only the hand-in exercises (“Abgabe”) are relevant. You can find the respective deadline on the exercise sheets.

## Final exam

- The first final exam is on 11.09.2017 at 8:30 in room 42-115.
- The second final exam is on 13.10.2017 at 8:15 in the Mensa.
- You have to register for the final exam at the Prüfungsamt (examination office) at least 2 weeks before the date of the exam.
- You can find the syllabus of the “Theoretic Computer Science Amendment”-version of Logic in the Modulhandbuch, Module 89-5021. Note that Gentzen sequent calculus for propositional logic and the Tableaux method in predicate method are not included in the syllabus. (The Tableaux method for propositional logic is included!)
We have reserved room 48-453 in the two weeks before the first final exam (i.e. 28.08.-08.09.). During this time you can use this room for preparing for the exam together with other students. We will be available there for questions at the following times:

- Thursday, 31.08. 14:00-15:00
- Tuesday, 05.09. 15:00-16:00
- Thursday, 07.09. 14:00-15:00
- Friday, 08.09. 14:00-15:00

These times might still change, so check this page before coming.

## Support session

We offer an additional support session, where you can ask individual questions and get support on exercise tasks. The session is Mondays at 13:45 in room 48-379.

## Mid-term exams

The mid-term exam is on 19.06.2017 at 19:00 in room 46-220. If you are taking the “Logik” lecture as part of the “Theoretical Computer Science Amendment”, you are not required to participate or pass the mit-term exam, but it is recommended to participate as preparation for the final exam. Please register for the exam “Zwischenklausur - Logik - SS17” via Mail to Peter Zeller if you want to participate.

### Details

- Duration: 100 minutes
Content: Everything including the lecture on the June 14. and exercise sheet 9.

The optional exercise about Isablle on sheet 4 is not part of the exam.- You are allowed to bring:
- One DIN A4 sheet of paper with own hand-written notes (on both sides)
- Language dictionaries

## Final exams

You have to register for the final exam at the Prüfungsamt (examination office). Please also register via Mail to Peter Zeller so that we can prepare an English translation of the exam for you.

The first final exam will take place on 11.09.2017 at 8:30 in room 42-115.

The second final exam will be on 13.10.2017 at 8:15 in the Mensa.