## Module Handbook

• Dynamischer Default-Fachbereich geändert auf INF

# Course INF-02-05-K-2

## Course Type

SWS Type Course Form CP (Effort) Presence-Time / Self-Study
- K Lecture with exercise classes (V/U) 6.0 CP 110 h
3 V Lecture 42 h
2 U Exercise class (in small groups) 28 h
(3V+2U) 6.0 CP 70 h 110 h

## Basedata

SWS 3V+2U 6.0 CP = 180 h 1 Sem. in WiSe [2] Bachelor (Fundamentals) [DE] German Lin, Anthony, Prof. Dr. (PROF | DEPT: INF) [INF-PFL] Mandatory Modules [NORM] Active

## Possible Study achievement

• Verification of study performance: proof of successful participation in the exercise classes (ungraded)
• Details of the examination (type, duration, criteria) will be announced at the beginning of the course.

## Contents

• Propositional logic
• Syntax and semantics
• Proof calculus of natural closure
• Tableau method
• Resolution procedure, Davis-Putnam procedure
• First-level predicate logic
• Syntax: Predicates, Functions, Quantors
• Semantics: interpretations, occupations, evaluations,
• Compact theorem and Herbrand universe
• Sentences from Löwenheim and Skolem
• Semi-decidability
• First level theories: Decidability
• Gödel's incompleteness sentence
• Proof calculus and automatic proofers
• Tableau and resolution procedure
• SMT Solver
• higher level predicate logic
• Type theory
• Axiom and proof systems
• Interactive theorem provers
• Logical programming and Prolog
• SLD resolution
• Fixed-Point Semantics and Negation as Failure
• Program verification
• Axiomatic Semantics and Hoare Calculus
• Denotational Semantics and Weakest Preconditions

## Literature

• Sperschneider, Antoniou: Logic - A Foundation for Computer Science, Addison Wesley.
• Nissanke: Introductory Logic and Sets for Computer Scientists, Addison Wesley.
• Kreuzer, Kühling: Logik für Informatiker, Pearson Studium.

None

## References to Course [INF-02-05-K-2]

Module Name Context
[INF-02-05-M-2] Logic and Semantics of Programming Languages P: Obligatory 3V+2U, 6.0 LP
[INF-82-51-M-2] Formal Foundations of Computer Science P: Obligatory 3V+2U, 6.0 LP