University of Leicester


Computer Science Internal Seminars

The Internal Seminar Series is a relaxed forum for members of the Department to present their current research and discuss ideas of interest. Invited speakers are also welcome, in particular for presentations that might be too specialised for a general computer science audience as on the Friday's seminar.

How to find the most common lecture rooms: See the External Seminar page.

Semester 2

Room this semester is BEN LT5. Most of the slots will be taken by the APG seminar.

Seminar programme

Seminar details

Product of Hybrid Logics (Slides)

Katsuhiko Sano (Kyoto University)
Fri, Jul 16, 14:00 in ATT SB2.07 (Host: Tadeusz Litak, Alexander Kurz)

Hybrid logic is an extended modal logic with nominals (a syntactic name of a state). In this talk, I will propose how to combine two hybrid logics, i.e., a way of dealing with two dimensions (e.g. time and space) at the same time in one setting. Our way of combining hybrid logics can be regarded as an extension of product of modal logic (Gabbay and Shehtman 1998). In the first part, I will explain how to `product' two hybrid logics over Kripke frames and establish a general completeness result (called pure completeness) for Kripke semantics. In the second part, I will extend this product method to hybrid logics over topological spaces and show that we can still keep a general completeness result. If time permits, I will also explain how to capture the dependence of one dimension (space) over the other (time).

On the termination of Russell's description elimination algorithm

Vincent van Oostrom (Utrecht)
Thu, Mar 18, 10:00 in BEN LT5 (Host: Fer-Jan de Vries)

We analyse the process of eliminating descriptions in predicate logic.

Semester 1

Room this semester is BEN LT5. Most of the slots will be taken by the APG seminar.

Seminar programme

Seminar details

Linear logic for graph transformation

Paolo Torrini (Leicester)
Fri, Nov 6, 11:00

We are looking into a way to represent name restriction as resource-bound quantification and DPO graph transformation as linear consequence relation, relying on a first-order variant of intuitionistic linear logic with proof terms.

A Theory of DbC for Multiparty Distributed Interactions (Slides)

Emilio Tuosto (Leicester)
Fri, Nov 6, 10:00

Universal algebra over nominal sets

Alexander Kurz (Leicester)
Thu, Nov 5, 16:00

(joint work with D. Petrisan) We study categories of algebras for endofunctors on Nom, the category of nominal sets in the sense of Gabbay and Pitts. We start from the fact that Nom is a full reflective subcategory of a monadic category, namely the presheaf category Set^I. We then show that the standard category theoretic proof of Birkhoff's HSP theorem can be `pushed through the adjunction' relating Nom and Set^I, thus yielding an HSP-theorem for nominal algebras. This theorem is different from the one proposed by Gabbay, and we show how to recover his theorem from ours by restricting the equational logic of universal algebra to what we call `uniform equations'. Whereas the first result is axiomatic in that it only depends on properties of the adjunction, the result on uniform equations is rather more specific to Nom and Set^I.

Nominal Kleene algebra

Tomoyuki Suzuki (Leicester)
Thu, Nov 5, 15:00

(joint work with Alexander Kurz and Emilio Tuosto) It is well known that Kleene algebras, finite automata and regular languages are considered as fundamental tools to describe machines and to analyse computation in Computer science. Nowadays, however, the meaning of machines or computations starts to contain "communications", "security" or "resources". In other words, computer is not only a stand alone machine but also a dynamic system which is sensitive to its own environment. Through this research, we try to capture the relatively new notion of machines with Nominal algebras, which allow us to clarify local and global information for each computer. In this talk, I will present our nominal languages, automata with names and Nominal Kleene algebras.

The trouble with names in graph transformation

Reiko Heckel (Leicester)
Thu, Nov 5, 14:00

In the standard categorical approach to graph transformation, the result of a rule application is only defied up to isomorphism. Rightly or wrongly, this leads to the perception that graphs should be considered up to isomorphism, ignoring the concrete names of their nodes and edges. We discuss some of the problems arising from this interpretation, touching on concurrent semantics, stochastic model checking and hint on the (sometimes ad-hoc) solutions.

Description Logics (Slides)

Paula Severi (University of Leicester)
Thursday Oct 8, 10:00 in Ben LT5

In this talk I will give an introduction to Description Logics. Description Logics (DLs) are decidable fragments of first order logic that are used in several application domains of Artificial Intelligence. The most sucessfull area of application is the semantic web. The Web Ontology Language (OWL) is based on a description logic.

Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356.
University of Leicester . Last modified: 9th February 2012, 21:21:19.
Informatics Web Maintainer. This document has been approved by the Head of Department.