1. General competences:
   • detect inconsistencies and mistakes in wrongly formulated statements
   • formulate clear, consistent and correct assertions
   • provide argumentation about the correctness of your own assertions
   • systematically derive solutions
   • take part actively and constructively in making unclear assertions clear
   • structurize text using definitions
   • indicate the distinctions between natural languages and formal languages
   • deal in a professional way with different notations for intrinsically the same language
2. Specific competences with respect to logic:
   • recognize which problems can be solved and which problems cannot be solved using propositional logic
   • translate natural language assertions into logic in a systematic way
   • present the semantics of formulas in propositional or predicate logic in a clear way in natural language
   • explain the semantics of the rules for natural deduction
   • prove assertions using natural deduction
   • present proofs in a comprehensible way
   • derive truth tables for assertions in propositional logic
   • derive semantic tableaux for assertions in propositional logic
   • use the terminology of tautology, logical consequences and logical equivalences
   • recognize and indicate mistakes within proofs
   • use the proof assistant Coq to prove theorems without reasonable doubt
3. Specific competences with respect to system modelling:
   • create a rationality square for a given artefact
   • specify important properties of simple real time systems and their components within predicate logic
   • prove correctness of specifications in predicate logic
   • divide systems hierarchically into their components
   • prove that a system complies to certain properties using specifications in predicate logic of its components
   • clearly present an analysis, a design and a correctness proof of a system

This is a course in applied logic. On the one hand you will learn how to specify systems both informally in natural language and formally using propositional or predicate logic. Our goal is to describe these systems in such a way that these specifications can be used as a contract. On the other hand you will learn how to prove these assertions, or in other words, to prove that these systems operate exactly as they should according to their contracts. This process of argumentation will also be done using natural language and using formal mathematical methods. Eventually you will use a proof assistant to check your proof.

These techniques will be practised in relatively small weekly exercises. They will be tested in written intermediate exams and a group project in which you will show that you can apply these techniques of assertion and argumentation on a complex system.