Seminar Koalgebraische Logik (WiSe 2015/16)

Dozent Lutz Schröder
Daten TBA
Zielgruppe WPF INF-MA 8 (ECTS-Credits: 5)
WPF INF-BA-V-THI (ECTS-Credits: 5)

(Geeignet als WPF für Nebenfach Informatik in verschiedenen Studiengängen, insbesondere Mathematik.)

In der logikbasierten Wissensrepräsentation und in der Spezifikation nebenläufiger Systeme werden heute vorwiegend modale Logiken verwendet. Wenn diese über die relationale Standardsemantik hinausgehen und über Dinge wie Zufall, ungefähres Wissen oder Koalitionen von Agenten reden, kann man mit Gewinn koalgebraische Logik verwenden, um Deduktionssysteme und Algorithmen durch Instanziierung generischer Off-the-Shelf-Resultate zu erhalten. Einen Überblick über das relativ junge Gebiet bietet dieses Seminar.

Termine ((sehr) vorläufig)

  • Ab 17.11.15: Paul Wild, The Finite Model Property
  • Ab 08.12.15: Martin Schmitt, PSPACE Reasoning
  • Ab 22.12.15: Ludwig Dietel, Coalgebraic EL
  • Ab 19.01.15: Hans-Peter Deifel, Coalgebraic Hybrid Logic

Themen

Die folgende Themenliste ist weder notwendigerweise erschöpfend noch wird sie zwingend vollständig abgearbeitet:

  • Kategorielle Grundlagen
  • Koalgebraische Logik via Prädikatenliftings
  • Ausdrucksstärke
  • Korrektheit und Vollständigkeit
  • Algebraische Semantik
  • Komplexität von Deduktionsproblemen
  • Modulare Konstruktion von Logiken
  • Koalgebraische Hybridlogik
  • Deduktion über TBoxes
  • Fixpunktlogiken
  • Koalgebraische Automatentheorie
  • Koalgebraische Fuzzy-Logiken
  • Koalgebraische Prädikatenlogik

Literatur

(Die folgende Liste ist als breit angelegter Literaturführer und nicht als verpflichtende Leseliste zu verstehen.)

  • 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)