-
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
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 | |
Lecturers | |
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
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
- 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 |