Dirk Pattinson

Professor, Director, ANU-ASD Co-Lab, and Associate Dean HDR

Interests

Research

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 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.

Biography

I’m a mathematician turned computer scientist. Prior to joining ANU I held a (senior) lectureship at Imperial College London, a lectureship at the University of Leicester and was a Research Associate at LMU Munich.

Activities & Awards

bars search times arrow-up