Bernhard Gramlich | AG Theoretische Informatik und Logik | Fakultät für Informatik | TU Wien

185.298
Computational Equational Logic, VU 3.0/2.0

Teacher: Bernhard Gramlich, gramlich@logic.at

The course "Computational Equational Logic" is an optional course in the new Computer Science Master Studies Computational Intelligence (Wahlfachkatalog "Theoretische Informatik und Logik") and Software Engineering & Internet Computing (Wahlfachkatalog "Theoretische Informatik") and is also part of the European Masters Program in Computational Logic (Advanced Modules / Inference in Classical and Non-Classical Logic).

The course will be held in English!

News

The course will be offered next time in the summer term 2010.
Registration for the course via TUWIS++ (till March 14, 2010) is possible here.
Dates:
- General preparatory meeting (joint with other courses of the Theory and Logic Group (E185/2)): Brief survey and organizational issues:
  Monday, 08.03.10, 11:30-12:30, Seminarraum Zemanek
- First class: Thursday, 11.03.10, 11:15-12:45, "Labor E185/2" near Seminarraum E185/2
  Note: In March while the Seminarraum von Neumann is not yet usable, the course will take place in "Labor E185/2" near Seminarraum E185/2!
- Regular date: Thursday, 11:15-12:45, Seminarraum von Neumann, Favoritenstr. 9-11, EG, Zugang vom Innenhof, Erdgeschoß
Combination/Deepening: In parallel to this course there will also be a Seminar in Theoretical Computer Science with thematic focus "Semantics of Programming Languages" in the summer term 2010. Some topics offered in this seminar are closely related to "Computational Equational Logic" via "Algebraic Semantics" (based on equational reasoning). Hence, participation in the seminar is recommended, too (but no precondition for attending the course)!

Contents of the course

This advanced course focuses on and deepens various aspects of the area Computational Equational Logic. Topics to be dealt with include e.g. extended notons of term rewriting, reduction and computation strategies, modular aspects of equational and rewrite systems, rule-based programming, equational theorem proving.

Students attending the course should acquire a deeper understanding in this area as well as get an impression of the importance of these theoretical foundations for applications in programming and deduction, as well as in specifying and verifying programs.

The course presupposes at least some basic knowledge in Term Rewriting Systems. Desirable, but not necessary, is background knowledge in Unification Theory.

Specialization Options and Perspectives

The course also offers a good basis for various possibilities of deepening studies in the field of Computational (Equational) Logic. This concerns students' projects in the context of Practical Courses, Seminars, Diploma and Master theses including potential topics for work on Ph.D. projects within some Ph.D. studies.

Course material

Copies of the slides used in the course and additional material will be made available.

Assessment

The practical part of the course is integrated and will take place in the form of homework solved independently and (partially) discussed later in the course. At the end there will be a final exam. The overall assessment takes into account not only the final exam, but als the homework and the general participation during the course.