Die Dozenten der Informatik-Institute der Technischen Universität Braunschweig laden im Rahmen des Informatik-Kolloquiums zu folgendem Vortrag ein.
Prof. Dr. Lutz Schröder, Friedrich-Alexander-Universität Erlangen-Nürnberg, Chair 8 – Theoretical Computer Science: Deduction in Coalgebraic Modal and Temporal Logics
Beginn: 19.02.2015, 14:00 Uhr Ort: TU Braunschweig, Informatikzentrum, Mühlenpfordtstraße 23, 1. OG, Hörsaal M 161 Webseite: http://www.ibr.cs.tu-bs.de/cal/kolloq/2015-02-19-schroeder.html Kontakt: Prof. Dr.-Ing. Ina Schaefer
Modal and temporal logics traditionally play a key role in core areas of computer science such as knowledge representation and specification and verification of reactive systems. Their traditional relational semantics provides a good fit for many applications, but needs to be extended in various directions if one wants to cover additional aspects such as uncertainty, counting (e.g. in redundancy analysis) or agency. This need is witnessed by the emergence of, e.g., probabilistic, graded, alternating-time and neighbourhood-based logics, which all go markedly beyond relational semantics in an effort to enhance the expressivity of verification logics. In this context, coalgebraic logic plays the role of a unifying semantic umbrella for such formalisms. On the basis of my work, coalgebraic logic has evolved from a purely semantic concept into an algorithmic framework offering a wide array of generic reasoning services that can easily be instantiated to individual logics; these results form the basis for the development of the Coalgebraic Ontology Logic Reasoner (COOL). Following an introduction to the basic concepts of coalgebraic logic, I will briefly discuss a key technical tool in coalgebraic logic, so-called one-step rules, and give an overview of generic reasoning procedures for coalgebraic logics based on one-step rules, with a particular focus on tractable reasoning in conjunctive fixpoint logics modelled on the description logic EL.