Koalgebraische Logik (CoLog)5 ECTS
(englische Bezeichnung: Coalgebraic Logic)
(Prüfungsordnungsmodul: Seminar Koalgebraische Logik)

Lehrveranstaltungen:

• • Seminar Koalgebraische Logik
    (Seminar, 2 SWS, Lutz Schröder, Do, 14:15 - 15:45, 00.131-128)

Empfohlene Voraussetzungen:

Basic knowledge in logic, ideally some acquaintance with modal logic.

Inhalt:

• Basic categorical notions
  

• Coalgebraic logic via predicate liftings
  

• Separation and expressivity
  

• Soundness and completeness
  

• Algebraic semantics
  

• Complexity of reasoning
  

• Modular construction of logics
  

• Coalgebraic hybrid logic
  

• Reasoning with global assumptions
  

• Fixpoint logics
  

• Coalgebraic automata theory
  

• Fuzzy coalgebraic logic
  

• Coalgebraic predicate logic
  

Lernziele und Kompetenzen:

Fachkompetenz

Wissen

Die Studierenden geben grundlegende Definitionen und Resultate zu Koalgebra, Modallogik, und koalgebraischer Logik wieder und ordnen Beispiele korrekt ein.

Verstehen

Die Studierenden erläutern generische Schlussfolgerungsverfahren und algorithmische Verfahren in der koalgebrischen Logik und instanziieren sie auf konkrete Logiken.

Anwenden

Die Studierenden übertragen koalgebraische generische Verfahren selbständig auf Beispiele.

Erschaffen

Die Studierenden bereiten Resultate des Gebiets und ihre Herleitung eigenständig zur Präsentation auf.

Lern- bzw. Methodenkompetenz

Die Studierenden erarbeiten sich selbständig den Inhalt wissenschaftlicher Veröffentlichungen und geben diesen in einem strukturierten Vortrag verständlich wieder.

Sozialkompetenz

Die Studierenden arbeiten in einer größeren Gruppe an komplexen Problemen und erläutern eigene Einsichten den Mitstudierenden in verständlicher Form.

Literatur:

(The following list is, while not exhaustive, meant mainly as a fairly broad guide to the literature, and not to be understood as a mandatory reading list.)

• Lawrence S. Moss: Coalgebraic Logic. Ann. Pure Appl. Logic 96(1-3): 277-317 (1999)

• Dirk Pattinson: Expressive Logics for Coalgebras via Terminal Sequence Induction. Notre Dame Journal of Formal Logic 45(1): 19-33 (2004)

• Dirk Pattinson: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309(1-3): 177-193 (2003)

• Lutz Schröder: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Program. 73(1-2): 97-110 (2007)

• Lutz Schröder, Dirk Pattinson: Shallow Models for Non-iterative Modal Logics. KI 2008: 324-331

• Dirk Pattinson, Lutz Schröder: Beyond Rank 1: Algebraic Semantics and Finite Models for Coalgebraic Logics. FoSSaCS 2008: 66-80

• Lutz Schröder: Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci. 390(2-3): 230-247 (2008)

• Lutz Schröder, Dirk Pattinson: Strong Completeness of Coalgebraic Modal Logics. STACS 2009: 673-684

• Robert S. R. Myers, Dirk Pattinson, Lutz Schröder: Coalgebraic Hybrid Logic. FOSSACS 2009: 137-151

• Lutz Schröder, Dirk Pattinson, Clemens Kupke: Nominals for Everyone. IJCAI 2009: 917-922

• Lutz Schröder, Yde Venema: Flat Coalgebraic Fixed Point Logics. CONCUR 2010: 524-538

• Lutz Schröder, Dirk Pattinson: Description Logics and Fuzzy Probability. IJCAI 2011: 1075-1081

• Tadeusz Litak, Dirk Pattinson, Katsuhiko Sano, Lutz Schröder: Coalgebraic Predicate Logic. ICALP (2) 2012: 299-311

• Daniel Gorín, Lutz Schröder: Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics. Advances in Modal Logic 2014: 254-273

• Daniel Gorín, Dirk Pattinson, Lutz Schröder, Florian Widmann, Thorsten Wißmann: COOL - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description). IJCAR 2014: 396-402

• Corina Cîrstea, Clemens Kupke, Dirk Pattinson: EXPTIME Tableaux for the Coalgebraic mu-Calculus. Logical Methods in Computer Science 7(3) (2011)

• Yde Venema: Automata and fixed point logic: A coalgebraic perspective. Inf. Comput. 204(4): 637-678 (2006)

• Clemens Kupke, Yde Venema: Coalgebraic Automata Theory: Basic Results. Logical Methods in Computer Science 4(4) (2008)

• Stefan Milius, Dirk Pattinson, Lutz Schröder: Generic Trace Semantics and Graded Monads. CALCO 2015: 253-269

• Clemens Kupke, Dirk Pattinson, Lutz Schröder: Reasoning with Global Assumptions in Arithmetic Modal Logics. FCT 2015: 367-380

• Lutz Schröder, Dirk Pattinson, Tadeusz Litak: A Van Benthem/Rosen theorem for coalgebraic predicate logic. J. Log. Comput. 27(3): 749-773 (2017)

• Daniel Hausmann, Lutz Schröder: Optimal Satisfiability Checking for Arithmetic \mu -Calculi. FoSSaCS 2019: 277-294

• Daniel Hausmann, Lutz Schröder: Game-Based Local Model Checking for the Coalgebraic mu-Calculus. CONCUR 2019: 35:1-35:16

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:

1. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Hauptseminar | Seminar Koalgebraische Logik)

Studien-/Prüfungsleistungen:

Seminar Koalgebraische Logik (Prüfungsnummer: 31591)

Prüfungsleistung, Seminarleistung, benotet, 5 ECTS

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die Prüfungsleistung besteht in einer Ausarbeitung und einem 90-minütigen Vortrag. Der Vortrag kann im Rahmen regelmäßiger Videokonferenzen in elektronischer Form gehalten werden.

Prüfungssprache: Deutsch und Englisch

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

1. Prüfer:

Lutz Schröder