Research Interests
- modal logics, in partiular coalgebraic semantics, automated reasoning
- domain theory, in particular computation over continuous data
- logic and category theory in general
Overview
My research is broadly concerned with applications of logic in
computer science. In particular, my interest lies in the foundations
of computations with infinite objects (e.g. exact real numbers) and
their logical analysis (e.g. infinite behaviour of computational
systems). The main application that I am pursuing at the moment is
logic-based knowledge representation. This involves to formalise
knowledge in a particular application domain in terms of logical
formulae, which can then be used to check e.g. consistency of
hypotheses against the (formalised) background knowledge. The main
novelty here lies in the fact that the approach taken here allows
for a compositional integration of a large number of reasoning
principles such as e.g. probabilistic information of non-monotonic
conditionals.
Computation with Real Numbers
Together with Abbas Edalat (also Imperial College London) I have
developed domain-theoretic methods for solving
differential equations. This results in a computational framework
where solutions of differential equations can be obtained up to an
aribtrary degree of accuracy, and free of round-off errors.
Subsequently, a model of differential calculus has been developed
that allows the use of derivatives of Lipschitz functions, i.e.
functions that do not have a classical derivative. The use of this
form of derivatives is not available in standard approaches, and
greatly increases computation speed and accuracy.
Coalgebras and Modal Logic
Coalgebras are the formal dual of algebras and provide models of
infinitely recurring phenomena such as real numbers (infinite
decimal expansions) as well as various models for state-based
systems (that exhibit infinite behaviour).
I have developed a uniform logical framework that
allows to analyse and reason about a large class of structurally
different systems in a uniform way. Importantly, the coalgebraic
framework is inherently compositional: one can e.g. synthesise a
logic to reason about games with quantitative uncertainty from a
logic for games and probabilistic modal logic. I have contributed to
the extension of the basic framework to more expressive (modal)
logics such as hybrid logic and the coalgebraic mu-calculus, to the
general theory of automated reasoning with coalgebraic logics.,
Modal Logics for Knowledge Representation
Modal logics are (by and large) succinct, yet expressive, and still
decidable. This has spawned interest in the use of modal logics for
representing knowledge. The art of using modal logics for knowledge
representation is usually subsumed under the name
decription
logic which is mostly a notational variant of modal logic.
However, description logics have two important features: first, they
allow to speak about individuals (and thus name particular states in
a model) and usually come with a well-developed theory of global
consequence (and allow us to restrict attention to a specific class
of models that are of interest for specific application areas). As
it stands, description logics are well-developed over relational
semantics. On the other hand, many problems in knowledge
representation require languages that are more feature-rich: the
main example is the ability to reason about probabilities. Given
that feature-rich logics can be synthesised coalgebraically (see
above), the next natural question is how this can be exploited
fruitfully for puproses of knowlede representation.
Survey Paper
For a largely non-technical introduction to all things coalgebraic
and logical, see the paper
Modal Logics are
Coaglebraic that was written in response to a call for papers
for the conference
Visions in
Computer Science, held at Imperial College London in 2008.