COMPUTER SCIENCE COLLOQUIUM
Hybrid Logic
Torben Braüner
Programming, Logic and Intelligent Systems Group
Roskilde University
Tuesday, 01 September, 2009 at 14:15
IMADA's Seminar Room
ABSTRACT
Hybrid logics are a principled generalization of both modal logics and
description logics, a standard formalism for knowledge representation.
Hybrid logics allow direct reference to worlds/times/states or whatever the
elements of the model (a graph) are meant to represent.
It is easy to justify interest in hybrid logic on applied grounds, because
of the usefulness of the additional expressive power. For example, when
reasoning about time one often wants to build up a series of assertions
about what happens at a particular instant, and standard modal formalisms do
not allow this. What is less obvious is that the route hybrid logic takes to
overcome this problem often actually improves the behavior of the proof
procedures. For example, it is far simpler to formulate natural deduction
systems in hybrid logic than in ordinary modal logic.
In my talk I describe essential proof-theoretical results for a natural
deduction formulation of hybrid logic. The natural deduction system is
extended with additional inference rules corresponding to conditions on the
model expressed by so-called geometric theories. Thus, I give natural
deduction systems in a uniform way for a wide class of hybrid logics. This
shows that hybrid logics are a viable enterprise and opens up the way for
future applications.
Host: Kim Skak Larsen
SDU HOME |
IMADA HOME |
Previous Page
Daniel Merkle