Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Course INF-02-05-K-2

Logic and Semantics of Programming Languages (3V+2U, 6.0 LP)

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
CP, Effort 6.0 CP = 180 h
Position of the semester 1 Sem. in WiSe
Level [2] Bachelor (Fundamentals)
Language [DE] German
Lecturers
Area of study [INF-PFL] Mandatory Modules
Livecycle-State [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.

Requirements for attendance (informal)

Courses

Requirements for attendance (formal)

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