Nonclassical Logics in Computer Science (NoCL)7.5 ECTS
(englische Bezeichnung: Nonclassical Logics in Computer Science)
(Prüfungsordnungsmodul: Nonclassical Logics in Computer Science)

Lehrveranstaltungen:

• • Nonclassical Logics in Computer Science
    (Vorlesung mit Übung, 4 SWS, Tadeusz Litak et al., Mo, Di, 12:15 - 13:45, 01.255-128; Raumreservierung bleibt zunächst bestehen. Veranstaltung wird nach Möglichkeit in Präsenz angeboten, bei Bedarf mit digitalem Zusatzangebot, etwa Liveübertragung per Zoom.)

Inhalt:

The course overviews non-classical logics relevant for computer scientists, in particular

• Modal logics, extended to formalisms for reasoning about programs - PDL, mu-calculus. Modal systems also form the core of logics of agency and logics for reasoning about knowledge. Moreover they can be seen as a computationally well-behaved fragment of first-order logic over relational structures.
  

• Intuitionistic logic, which can be seen as a fragment of certain modal logics (S4) or as the logic of type theory and program extraction.
  

• Linear logic, which is established as the core system for resource-aware reasoning
  

• The logic of bunched implications and separation logic: more recent formalisms to reason about heap verification and programs involving shared mutable data structures.
  

• Fuzzy and multi-valued logics for reasoning with vague information.
  

Lernziele und Kompetenzen:

Fachkompetenz

Wissen

Students reproduce definitions and results on nonclassical logics.

Verstehen

Students explain and compare logical principles required for modelling and reasoning about different computational phenomena (e.g. resource-awareness, vagueness, program execution).

Anwenden

Students use formal tools (semantics and proof-theoretical calculi) to establish the validity of given propositions in computationally relevant systems of non-classical logic

Analysieren

Students conduct metatheoretical proofs on nonclassical logics, investigating the issues of decidability, completeness, complexity and other issues like interpolation. They translate between systems when possibly, e.g., from classical to intuitionistic or from intuitionistic to modal logic.

Evaluieren (Beurteilen)

Given an application problem in computer science, students identify the right logical apparatus to solve the problem.

Lern- bzw. Methodenkompetenz

Students conduct formal proofs.

Sozialkompetenz

Students work efficiently in small teams.

Literatur:

• Patrick Blackburn, Maarten de Rijke, Yde Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. 2002
  

• Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press 1997
  

• David Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, 2002.
  

• Greg Restall. An Introduction to Substructural Logics, Routledge 2000
  

• Nick Galatos, Peter Jipsen, Tomasz Kowalski, Hiroakira Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier 2007

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:

1. Informatik (Master of Science)
   (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Gesamtkonto | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsrichtung Theoretische Informatik | Nonclassical Logics in Computer Science)

Studien-/Prüfungsleistungen:

Nonclassical Logics in Computer Science (Prüfungsnummer: 31251)

Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, benotet, 7.5 ECTS

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer mündlichen Prüfung am Semesterende und zu 50% aus der Bewertung der Leistungen aus dem Übungsbetrieb zusammen.

Prüfungssprache: Englisch

Erstablegung: WS 2020/2021, 1. Wdh.: SS 2021

1. Prüfer:

Tadeusz Litak