Computational Logic
On this page information about the Computational Logic stream in the master program of the Institute of Computer Science is provided.
A list of possible master project topics is available.
Curriculum
The following courses will be offered:
The red courses are compulsory. Moreover, at least one blue course course and at least two green seminars must be chosen. To obtain the required 22 units, in addition to the courses offered by the Computational Logic group, courses from the following (preliminary) list may also be chosen:
| Coding Theory and Cryptology | VO2 + UE1 | SS 2007 | (Institute of Mathematics) |
| Ontology Engineering | VU2 | SS 2007 | (DERI) |
| Semantic Web | VU4 | SS 2007 | (DERI) |
| Kombinatorik | VO4 + PS2 | SS 2006 | (Institute of Mathematics) |
| Zelluläre Automaten | VO2 + PS1 | SS 2006 | (Institute of Mathematics) |
| Introduction to Artificial Intelligence | VO2 + UE2 | SS 2005 | (DERI) |
| Specification of Distributed Systems | VU2 | SS 2005 | (QE) |
| Advanced Topics of Web Technologies: Introduction to Logic Programming |
VU3 | WS 2004 | (DERI) |
Many of the courses in the Computational Logic stream are concerned with logic or rewriting.
Logic
Logic is the science of the argument and mathematical logic is the
science of the mathematical argument.
(J.R. Shoenfield, "Mathematical Logic")
Why should a computer scientist be knowledgeable in this subject?
Concepts and methods of logic occupy a central place in computer
science, insomuch that logic has been called
the calculus of computer science.
(P.G. Kolaitis and M.Y. Vardi)
The reason for the success of logic in computer science seems to be that logic serves the same part for computer science, that mathematics serves for physics: It provides a rigid, but flexible language to express the rich and diversified field of everything that is labelled "computer science".
How, if not with reference to the research in logic, could we know about the limitations of computing, about the (un)decidability and the complexity of certain problems that may well appear in practice? How, if not with formal methods can we make sure that our code meets its specifications? How, if not with the sharpened attention we get for free when we study theory, will we be able to design, maintain, or improve highly complex systems?
Courses with a strong logic content
- Automated Theorem Proving (in Isabelle/HOL)
- Modal and Temporal Logic
- Verification using Model Checking
Rewriting
Equational reasoning is an important component in symbolic algebra, automated deduction, high-level programming languages, program verification, and artificial intelligence. Reasoning with equations involves deriving consequences of given equations and finding values for variables that satisfy a given equation. Rewriting is a very powerful method for dealing with equations.
Directed equations, called rewrite rules, are used to replace equals by equals, but only in the indicated direction. The theory of rewriting centers around the concept of normal form, an expression that cannot be rewritten any further. Computation consists of rewriting to a normal form; when the normal form is unique, it is taken as the value of the initial expression. When rewriting equal terms always leads to the same normal form, the set of rules is said to be convergent and rewriting can be used to check for equality.
Rewriting is a Turing-complete computational model which is very close to functional programming. It has applications in algebra, recursion theory, software engineering, and programming languages. In general, term rewriting applies in any context where efficient methods for reasoning with equations are required.
Courses with a strong rewriting content
Our ideal student
- wants to understand more about the foundations and limitations of computers
- is not afraid of theory
- likes to program in a high-level programming language
- might want to pursue a career in research