Bernhard Gramlich | AG Theoretische Informatik und Logik | Fakultät für Informatik | TU Wien
Lecturer: Bernhard Gramlich (firstname.lastname@example.org)
Description of the course in TISS: 185.298 Computational Equational Logic.
The course "Computational Equational Logic" is part of the Computer Science Master Studies Computational Intelligence and Software Engineering & Internet Computing. It is also included in the European Masters Program in Computational Logic (Advanced Modules / Inference in Classical and Non-Classical Logic).
The course will be held in English!
This advanced course focuses on and deepens some 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, and semantics of equational / functional / functional-logic programs.
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 assumes some basic knowledge in Term Rewriting Systems. However, at the beginning of the course a summary of this knowledge will be presented in concise form. Thus, seriously interested students who did not yet attend Term Rewriting Systems can also participate provided they manage to understand and work through these basics. Desirable, but not necessary, is background knowledge in Unification Theory.
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 the course Project in Computational Logic (185.302, PR, 2011S , 8.0h) within the European Masters Program in Computational Logic, as well as of other Practical Courses, Seminars, Diploma and Master theses including potential topics for work on Ph.D. projects within some Ph.D. studies.
Copies of the slides used in the course and additional material will be made available.
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.