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.

IMPORTANT: The course presuposes some previous knowledge of Logic (e.g. TIL). Additional classes (Repetitorium) will be provided for students who need to refresh or consolidate their knowledge.

• 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

• 38 hours:  lecture time (+ 8 hours repetitorium  for students not having a firm previous knowledge in logic)
• 52 hours: 4 blocks of problems/exercises 
• 60 hours: examination (preparation time)

First class: Oct 5, 12:00 (sharp), room EI 1 Petritsch,  Elektrot.Institutsgebäude (Gußhausstr. 25-29) - 2. Stock (no class on Oct 2)

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

(see lecture slides for additional literature)

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),  and automata theory (finite automata, pushdown automata, Turing machines)

NB: If you don't have a firm background in logic yet, you are ask to join special repetitorium classes, which are open to all participants.