TU München | Informatik | Software & Systems Engineering | Theorem Proving Group | Lehre |

- Module:
- IN2049
- When and where:
- Mo. 08:30 - 10:00, Do. 14:15 - 15:45, Room: MI HS 2
- Start:
- 16. 10. 2008
- Exercises:
- Fr. 14:15 - 15:45, Room: MI 01.11.018 ("Konrad Zuse")
- Exam:
- Thursday, Feb 12th, 14:00 -
**16:00**, MW 0350

The exam will be**open book**.

Upon request, there is the possibility to take an oral exam for those students who failed the exam. - Tutors:
- Alexander Krauss, Sascha Böhme

- The exam results are available (please ask).

The course will be an introduction to logic, the basic language of all sciences. You will learn about the precise syntax and meaning of the standard logical language, first-order logic. What is more, you will also learn about automatic procedures for deciding logical formulae: from surprisingly efficient decision procedures for propositional logic to semidecision procedures for full first-order logic. These algorithms will be presented as actual code in OCaml, both in the lectures and the exercises. An understanding of OCaml is essential to follow the course.

Syllabus:

- Propositional logic
- Syntax, semantics, tautology, satisfiability, substitution
- Normal forms: NNF, DNF, CNF, definitional CNF
- Decision procedures: Resolution, DPLL
- Sequent calculus, soundness, completeness
- Compactness

- First-order logic
- Syntax, semantics, validity, satisfiability, substitution
- Normal forms: prenex, Skolemization
- Herbrand models, Herbrand's theorem, Gilmore's procedure
- Unification
- Resolution
- Undecidability
- Sequent calculus, soundness
- Equality

- Decision procedures
- AE and monadic class
- Finite model property
- Dense linear orders
- Linear real arithmetic
- Linear integer arithmetic (Presburger arithmetic)

Practical exercises in OCaml will complement the lectures and theory exercises. You will need some very basic knowledge of OCaml (for example from earlier lectures), or you should be prepared to learn this in the first weeks (here is some help).

We will make use of the code that comes with John Harrison's
book. Download
it here.
Before using it, you need to build it using *make*. If you are running Windows and don't have the *make* tool,
just download atp_interactive.ml (the result of the build process) and place it in
the code directory.

The exercises will include three small projects where you will program small logic-related tools. You can gain a bonus of one level (0.3) on your final grade if you complete one of the projects and a second bonus of two levels (0.6) if you complete at least two of them.

For the exercise sessions, please bring your laptop if you have one, and **make sure that you have OCaml running and the code downloaded**.

- Exercise 1: [ pdf ]
- Exercise 2: [ pdf ] Solution: [ pdf ] [ ex2.ml ]
- Exercise 3: [ pdf ] [ proofcheck.ml ] Solution: [ pdf ] [ ex3.ml ]
- Mini-Project 1: [ pdf ]
[ sudoku.ml ]
[ sudokus.txt ]

Solution: [ proj1.ml ] Some interesting test cases: [ custom_sudokus.txt ] - Exercise 4: [ pdf ] Solution: [ pdf ]
- Exercise 5: [ pdf ] Solution: [ pdf ]
- Exercise 6: [ pdf ] Solution: [ pdf ]
- Exercise 7: [ pdf ] Solution: [ pdf ]
- Exercise 8: [ pdf ] Solution: [ pdf ]
- Mini-Project 2: [ pdf ]
- Exercise 9: [ pdf ] Solution: [ pdf ]
- Exercise 10: [ pdf ] Solution: [ pdf ]
- Exercise 11: [ pdf ] Solution: [ pdf (corrected 11.4) ]
- Exercise 12: [ pdf ] Solution: [ pdf ]
- Mini-Project 3: [ pdf ]
- Exercise 13: [ pdf ] Solution: [ pdf ]

- John Harrison. Handbook of Practical Logic and Automated Reasoning. We will provide hardcopies of the relevant parts.
- For sequent calculus:
- Jean Gallier. Logic for Computer Science. (Chapter 3)

- Egon Börger, Erich Grädel, Yuri Gurevich. The Classical Decision Problem.
- Some slides.