After successful completion of the course, students are able to deal with logical calculations of the resolution system and other forms of automatic proof; regular and context-free languages; finite automata and turing machines as well as with aspects of the complexity theory.
The lecture starts with an introduction to the theory of finite automata and
formal languages. We get to know the classes of regular and context-free
languages, as well as various formalisms for defining such languages, in
particular finite automata and formal grammars. In the second part, after a
significant leap in expressivity, we will deal with computability theory, i.e.,
the question which functions are computable in principle. We use the operator
representation of partial recursive functions as well as Turing-machines. We
discuss the Church-Turing thesis and prove the foundational results of
computability theory. In the third part we consider computational complexity
theory which is obtained from computability theory by restricting the resources
which are available to a computation, e.g. to polynomial time. The P vs. NP -
problem belongs to this subject and will form the centre of our discussion of
computational complexity. In a final fourth part we will consider the
theoretical foundations of program verification which allows the application
and combination of several results from the previous parts.
