Equational Logic

Holger Gast, Sommersemester 2013


Contents (Last Year)

This lecture exclusively treats equational logic instead of the usual first-order logic. It combines the topics term-rewriting and lambda-calculus with a logical view.


  • Term Rewriting Animated To get an intuition of rewriting, try out the steps in our visualization! Available for Linux, Window, Mac OS.
    Alternatively, just download any Eclipse (Indigo/Juno) and install the software through the update site:
    (Menu: Help/Install Software)
    The source code is available from the Mercurial repository (see hg clone below) in subdirectory animated/eclipse. Use Eclipse Indigo (with PDE feature installed) to compile and run.
  • The cheat sheet summarizes the definitions given in the lecture to keep a handy overview throughout. It gets extended as we go along.


If you use the Mercurial version control system, you can synchronize these files automatically: hg clone https://www4.in.tum.de/~lammich/hg/logics_website
[ view changelog ]



There will be a written exam. It will last 120 minutes. You are allowed to bring one A4 sheet with your notes into the exam, books are not allowed.

There will be weekly homework sheets, which will be graded. Students who achieve 50% of the homework points will receive a bonus mark of 0.3, provided that they also pass the final exam.


Primary: Additional: