Vorträge im WS 2013

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet Dienstags von 14:15-15:45 in Raum 11.150-113 in der Martensstr. 3 statt. Es steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen. Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Nachfragen gerne per Mail an den Leiter des Lehrstuhls (mailto:lutz.schroeder@informatik.uni-erlangen.de).

Voraussichtlicher Plan für WS 2013

Bisherige Vorträge


Date	Speaker, Topic	Abstract
4-Feb	Ray-Ming Chen, //Full Rough Sets //	In the real world, most of the time, we do reasoning or inferences based on imperfect information or data. Such inferences must accomodate uncertainty and vagueness. In 1982, Pawlak introduced rough sets to approximate a crisp set based on indiscernibility relation. In this talk, I will use full rough sets (frs) to lift his restriction on the data-driven reasoning and study the properties (in particular, the closedness) of frs. In the end, I will also introduce probabilistic sets and fuzzy sets and their relationships with frs.
28-Jan	Ulrich Dorsch, //Succinctness Results for various Extensions of Multimodal Logic //	One possibility for the comparison of logics is their succinctness; for a fixed set of properties, the shorter formulas in a logic expressing these properties can be, the more succinct the logic is. In [1] T. French et al. presented several succinctness results using games to find formulas of minimum size separating large sets of models. In the first part of my master thesis, I reproduce these results using similar but more compact methods to find shortest modal descriptions presented in [2]. In this talk I will describe these methods and show results for some extensions of multimodal logic. [1] T. French et al. On the succinctness of some modal logics. http://cgi.csc.liv.ac.uk/~wiebe/pubs/Documents/ARTINT2699.pdf [2] S. Figueira, D. Gorín. On the size of shortest modal description. http://www8.cs.fau.de/~gorin/papers/aiml10.pdf
21-Jan	Anuj Dawar, //Fixed-point Approximations of Graph Isomorphism //	The problem of deciding if two graphs are isomorphic is a well-studied problem in computational complexity that is neither known to be in P nor known to be NP-complete. There are families of equivalence relations on graphs, which are known to over-approximate isomorphism, which are decidable in polynomial time. One such family, the Weifeiler-Lehman equivalence relations, has a number of equivalent characterisations arising in logic, algebra and combinatorics, and can be naturally described as the greatest fixed-points of natural refinement operators. In this talk review these various characterisations and examine refinements of the family of relations that are obtained by considering coherent algebras over finite fields. This is joint work with Bjarki Holm.
17-Dec	Christoph Rauch, Handling Algebraic Effects and a Bit of Generic Hoare Logic	Large portions of current programming theory and practice are based on algebraic notions of effect. One such concept is the recently developed paradigm of handling underspecified algebraic operations, as embodied in the Eff programming language. This is closely related to more well-established notions of monad-encapsulated side-effecting programs. The ultimate goal of this work is to establish a verification framework for a programming language with handling for algebraic operations. Our focus shifted, however, when we realized that the presence of a looping construction in the language posed the greater challenge. In this talk, I will introduce the vast corpus of concepts necessary for a generic Hoare logic for order-enriched effects with looping and handling for underspecified algebraic operations.
10-Dec	Daniel Gorin, An imperfect introduction to imperfect information logics	Starting with Henkin’s logic of branching quantifiers, several formalisms have been studied that allow to break the linear dependencies between quantified variables in first-order logic, one of the best known examples being Hintikka and Sandu’s Independence Friendly logic. The term “imperfect information logics” is sometimes used to refer to this family of logics, alluding to the fact that their semantics can be given in terms of games of imperfect information. In this introductory talk we will meet some of this logics and discuss their basic (sometimes rather unusual) properties.
3-Dec	Daniel Hausmann, Depth-1 coalgebraic fixed point logics – models	We continue our previous investigation of coalgebraic fixed point logics, i.e. logics which are obtained by extending basic coalgebraic modal logics with monotone predicate liftings by explicit (flat) fixed point operators, resulting in the coalgebraic definition of such logics as PLTL, CTL, ATL or graded modal logic with fixed point operators (depending on the original logic that we start from). Our central objective in this context is the provision of a correct solution to the satisfiability problem of such coalgebraic fixed point logics. We solve this task by first introducing a so-called focussing global-caching algorithm which employs a generic tableau-system in order to decide the problem and by consecutively proving the correctness of said algorithm. One direction of this proof involves the construction of a model coalgebra from the data generated by a successful run of the algorithm. Approaching a suitable model construction, we will first concern ourselves with a standard construction from modal logic, the so-called canonical model and see, why this relatively basic approach is by itself not adequate for the construction of (coalgebraic) fixed point models. We argue that a more involved method, namely the construction of a minimally defined tableau from a successful proof structure is required in order to ensure the actual satisfaction of least fixed point formulas in the candidate model coalgebra. We will again consider several illustrating examples in order to comprehend the involved structures and mechanisms.
26-Nov	Andre Kowollik, Mensch-Roboter Interaktion bei gestenbasierten Zweipersonenspiele: NAO spielt Schere, Stein, Papier	Zur Kommunikation und Interaktion zwischen Menschen gehört nicht nur die Sprache, sondern auch Mimik und Gestik. Serviceroboter die in Zukunft erfolgreich als Hilfe im alltäglichen Leben in die Gemeinschaft integriert und von den Menschen akzeptiert werden sollen, müssen daher bestimmte Voraussetzungen erfüllen. Darunter fällt die Fähigkeit Gesten zu erkennen und zu interpretieren, sowie, je nach Einsatzgebiet, die Anpassung an das soziale Umfeld. Eine Form der sozialen Interaktion ist, beispielsweise in der Kinderbetreuung oder in der Altenpflege, das gemeinschaftliche Spielen. Die Masterarbeit soll anhand von gestenbasierten Zweipersonenspielen (hier: Schere, Stein, Papier) aufzeigen, wie gut die Mensch-Mensch Interaktion auf Mensch-Roboter übertragbar ist.
19-Nov	Gabor Greif, Opetopic calculus: logic with higher-dimensional trees, [slides]	The recently discovered and formalized category O of opetopes (c.f. Baez and Dolan) appears to be an interesting starting point for ∞-categorical deduction systems, as coherence conditions automatically hold. I’ll introduce the construction behind the opetopes and discuss how it can be turned into a calculus. I’ll mostly follow the track laid out by Eric Finster at IAS. These notions appear useful for the future development of the Ωmega system (of Sheard et al.) with a sound and stratified logic fragment. For the curious: http://video.ias.edu/1213/univalent/0131-EricFinster
12-Nov	Tadeusz Litak, Relational Lattices	We study an interpretation of lattice connectives as natural join and inner union between database relations with non-uniform headers. We show that this interpretation proposed by database experts (Vadim Tropashko from Oracle) yields a class of lattices which has not been considered in the existing lattice-theoretical literature. We discuss axiomatizability and decidability of their (quasi-)equational theory and propose an equational axiomatization for a corresponding abstract algebraic class. It turns out that addition of just the “header constant” to the lattice signature already allows mimicking the Maddux technique for cylindric algebras and encode the word problem for semigroups in the quasiequational theory. Relational lattices, however, are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate standard contexts of relational lattices. In particular, we see that finite relational lattices, while not “bounded” in the McKenzie sense, are subdirectly irreducible.
5-Nov	Sergey Goncharov, (Co−) algebraic Automata Theory,	Coalgebra has been proven to offer a versatile abstraction layer for systematizing and reasoning about various aspects of systems, such as reactivity, observable behaviour, notions of equivalence, etc. Deterministic finite state machines were one of the first success stories inherently fitting the framework and the concept of coalgebra, for the notion of coalgebric bisimulation for them turned out to coincide with the standard textbook language equivalence. Defining trace semantics for systems for which this was not the case proved to be a rather more delicate task, which received a satisfactory treatment only recently with introduction of the generalized powerset construction. Here, we take this approach further and establish a notion of T-automaton, parametrized by an algebraic monad T, as a natural coalgebraic generalization of (non-)deterministic automata, push-down automata, (reactive) Turing machines, etc. Motivated by the equivalence of monads and theories, we introduce generic fixpoint expressions acting as a far reaching generalization of Kleene’s regular expressions. Furthermore, we prove a Kleene-style theorem about the equi-expressivity of automata and expressions.
29-Oct	Stefan Milius, Mathematical Operational Semantics and Finitary System Behaviour	Structural operational semantics is a popular and widely used framework for defining operational semantics by means of transition system specifications (tss). Syntactic restrictions on the format of tss, such as the GSOS format of Bloom, Istrail and Meyer ensure nice properties of operations specified by a tss (e.g. that bisimilarity is a congruence). In seminal work, Turi and Plotkin showed that tss can be generalized to the category-theoretic setting of distributive laws; in particular, they showed that tss in the GSOS format correspond precisely to distributive laws of a certain kind, formed from a functor S, representing the syntax of operations over a functor F, representing the transition type. This talk concerns a category-theoretic generalization of the “simple GSOS” format of Aceto. We will show that specifications in our generalized simple GSOS format induce operations preserving the behaviour of finite systems of type F; as applications we will see operations on regular languages, regular processes and weighted transition systems. We will also present a generalization of Aceto’s theorem, which states that the operational (term) model of a tss is locally finite, i.e. from every state of the model only a finite number of states are reachable by a sequence of transitions. Applying our result to the category of join-semilattices and appropriate functors S and F we obtain as a corollary Brzozowki’s result that the number of derivatives of a regular expression is finite modulo the join-semilattice equations.
22-Oct	Lutz Schröder, Universal Simulands and Subsumption Checking in Lightweight Coalgebraic Logics	While reasoning in logics extending a Boolean propositional base is necessarily at least coNP-hard, some families of specifically designed light-weight logics allow for tractable, i.e. polynomial-time reasoning, and hence may be expected to scale to large reasoning problems. One example of this type is the EL family of description logics; in this case, efficient reasoning may be based on simulation checking between suitable small models. In the current work, we lift this principle to the level of generality of coalgebraic logic. We thus not only identify tractable fragments of non-relational logics whose semantics features, e.g., neighbourhoods or integer weights, but we also obtain new insights in the standard relational setting, e.g. on polynomial-time reasoning with global assumptions in modal logics featuring only box and conjunction.
1-Oct	Dirk Pattinson, //Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5 //	Which modal logics can be `naturally’ captured by a sequent system? Clearly, this question hinges on what one believes to be natural, i.e. which format of sequent rules one is willing to accept. This paper studies the relationship between the format of sequent rules and the corresponding syntactical shape of axioms in an equivalent Hilbert-system. We identify three different such formats, the most general of which captures most logics in the S5-cube. The format is based on restricting the context in rule premises and the correspondence is established by translating axioms into rules of our format and vice versa. As an application we show that there is no set of sequent rules of this format which is sound and cut-free complete for S5 and for which cut elimination can be shown by the standard permutation-of-rules argument.
24-Sep	Hans-Christoph Kotzsch, Topos Semantics for Higher-Order Modal Logic	We present a semantic framework that allows defining models of higher-order modal logic in an arbitrary topos. The semantics differs from standard topos semantics of higher-order type theory due to the need to interpret modal operators. We will present and discuss in detail the formal system that is adequate for this semantics. We will also outline a completeness proof.