Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-02-05-M-2

Logic and Semantics of Programming Languages (M, 6.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-02-05-M-2 Logic and Semantics of Programming Languages 6.0 CP (180 h)
INF-02-05_MAT-M-2 Logic and Semantics of Programming Languages 5.0 CP (150 h)
Hint concerning Module INF-02-05_MAT-M-2:
Due to the previous knowledge acquired in the mathematical modules, students of the Bachelor's programme in Mathematics (with subsidiary field Computer Science) receive a reduced number of credit points for this module.

Basedata

CP, Effort 6.0 CP = 180 h
Position of the semester 1 Sem. in WiSe
Level [2] Bachelor (Fundamentals)
Language [DE] German
Module Manager
Lin, Anthony, Prof. Dr. (PROF | DEPT: INF)
Lecturers
Lin, Anthony, Prof. Dr. (PROF | DEPT: INF)
Area of study [INF-PFL] Mandatory Modules
Reference course of study [INF-82.79-SG] B.Sc. Computer Science
Livecycle-State [NORM] Active

Courses

Type/SWS Course Number Title Choice in
Module-Part 		Presence-Time /
Self-Study 		SL SL is
required for exa. 		PL CP Sem.
3V+2U INF-02-05-K-2
Logic and Semantics of Programming Languages
P 70 h 110 h
U-Schein
ja PL1 6.0 WiSe
  • About [INF-02-05-K-2]: Title: "Logic and Semantics of Programming Languages"; Presence-Time: 70 h; Self-Study: 110 h
  • About [INF-02-05-K-2]: The study achievement [U-Schein] proof of successful participation in the exercise classes (ungraded) must be obtained. It is a prerequisite for the examination for PL1.

Examination achievement PL1

  • Form of examination: written exam (Klausur) (90-120 Min.)
  • Examination Frequency: each winter semester
  • Examination number: 60205 ("Logic and Semantics of Programming Languages")

Evaluation of grades

The grade of the module examination is also the module grade.


Contents

From [INF-02-05-K-2] Logic and Semantics of Programming Languages:
  • 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

Competencies / intended learning achievements

The students
  • can apply the knowledge and methods of mathematical logic to the formal specification and verification of hardware and software systems,
  • understand the difference between syntactic derivations in proof calculus and the semantic concept of truth,
  • can explain the concepts of syntax and semantics using propositional and predicate logic,
  • may do their own proofs and review given proofs and patterns of proofs,
  • are able to use dedicated logic to open up special application areas,
  • can create formalizations using logical systems and formal proofs using proof systems.

Literature

From [INF-02-05-K-2] Logic and Semantics of Programming Languages:
  • 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)

Modules:

Requirements for attendance (formal)

None

References to Module / Module Number [INF-02-05-M-2]

Course of Study Section Choice/Obligation
[INF-82.79-SG] B.Sc. Computer Science Theoretical Foundations [P] Compulsory
[WIW-82.176-SG] B.Sc. Business Administration and Engineering specialising in Computer Science Engineering specialization - Computer Science [WP] Compulsory Elective

References to Module / Module Number [INF-02-05_MAT-M-2]

Course of Study Section Choice/Obligation
[MAT-82.105-SG] B.Sc. Mathematics Subsidiary Subject (Minor) [WP] Compulsory Elective