The course aims at a consolidation and extension of skills and knowledge in formal logic and the theory of computability; in particular in the use of logical formalisms as specification tools, of various logical systems for proof search, elements of modal logics and of intuitionistic logic, deeper understanding of the concept of computability, including its connections to logic and program verification.

• advanced aspects of classical first order logic as specification tool
• proof systems for classical first order logic, including  soundness and completeness proofs 
• elements of model theory (Löwenheim-Skolem, compactness, expressibility)
• principles of automated theorem proving
• methods for handling identity  
• comparison of types of inference systems 
• elements of modal logic: Kripke semantics, temporal logics 
• elements of intuitionistic logic and constructive proofs
•  computational aspects of logic
• undecidabilty of first order logic and its consequences
• models of computation (Turing machines, lambda calculus)
• elementary recursion theory
• Church-Turing thesis
• incompleteness of arithmetic and its consequences  

ETCS Breakdown:

6 ETCS = 150 hours

• 40 hours:  lecture time
• 90 hours: 5 blocks of problems/exercises (15 to 20 hours each)
• 20 hours: examination (incl. preparation time)

• five blocks of  problems/exercises (to be handed in separately)
• examination: written + oral

Knowledge of classical propositional logic and of basic concepts of classical first order logic (logical consequence, interpretations and model structures, satisfiability versus validity, acquaintance with various proof systems), a firm understanding of the syntax/semantic distinction, some experience with formal specification, acquaintance with a range of different programming paradigms (imperative, functional, logical), concepts of formal languages (grammars, Chomsky hierarchy) and automata theory (finite automata, pushdown automata, Turing machines)