 |
cms |
||
ABOUT |
Computer Science Internal SeminarsThe 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 2Room this semester is BEN LT5. Most of the slots will be taken by the APG seminar.Seminar programme
Seminar detailsProduct of Hybrid Logics (Slides)
Katsuhiko Sano (Kyoto University) 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) We analyse
the process of eliminating descriptions in predicate
logic.
Semester 1Room this semester is BEN LT5. Most of the slots will be taken by the APG seminar.Seminar programme
Seminar detailsLinear logic for graph transformation
Paolo Torrini (Leicester) 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) Universal algebra over nominal sets
Alexander Kurz (Leicester) (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.
Tomoyuki
Suzuki (Leicester) (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) 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.
Paula Severi (University of Leicester) 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. |
|