RSISE Buliding 115

The Australian National University

Canberra ACT 0200

Australia

E dirk.pattinson@anu.edu.au

T +61 (0)2 6125 8612

F +61 (0)2 6125 8651

The Australian National University

Canberra ACT 0200

Australia

E dirk.pattinson@anu.edu.au

T +61 (0)2 6125 8612

F +61 (0)2 6125 8651

Principal Investigator | Dirk Pattinson |

Start Date | Mar 1, 2010 |

Value | £ 396,787 |

Sponsor | Engineering and Physical Sciences Research Council (EPSRC) |

Reference | EP/H016317/1 |

Industrial Collaborator | The Microsoft Research-University of Trento Centre for Computational and Systems Biology |

Academic Collaborator | Rajeev Goré |

One Research Associate position and one PhD studentship available, starting March 2010. See below for job adverts.

Based on the framework of coalgebraic logic that I have introduced in my PhD thesis, the goal is to develop a generic, versatile and efficient automated reasoning tool that uniformly handles a large class of modal logics and their combinations. As a concrete case study, we apply this to the formalisation of problems in Systems Biology, based on case studies provided by the industrial collaborator, the Microsoft Research - University of Trento Centre for Computational and Systems Biology.

The main theme that underlies this research project is automated reasoning, an applied sub-discipline of mathematical logic. Logic has found applications in many areas of computer science such as the verification of digital circuits, reasoning about programs and knowledge representation. One of the most fundamental aspects in this context is to automatically decide whether a particular formula is a logical consequence of a given set of assumptions. The set of assumptions may describe complex relations between diseases and their symptoms, and one possible reasoning task would be to confirm or reject a diagnosis based on observed symptoms and medical history. In this research project, we investigate applications of mathematical logic in knowledge representation. One of the prime challenges in this area is to design logical formalisms that strike a balance between the two conflicting goals of expressiveness (the ability to formally represent the application domain) and computational tractability. The family of modal logics, conceived in a broad way, combines both aspects and serves as the mathematical foundation of a large number of knowledge representation formalisms. The core ingredient of modal logic is the possibility to qualify logical assertions to hold in a certain way. Depending on the context, we may for instance stipulate that assertion holds `always in the future', `with a likelihood of at least 50%' or `normally'. Together with names for individual entities, this allows us to formulate assertions like `the likelihood of congestion on Queen's Road is greater than 30%', and complex knowledge bases arise by combining different logical primitives. Automated reasoning then allows us to mechanically verify e.g. the consistency of scientific hypotheses against an existing knowledge base. Our goal is to build a modular and practical knowledge representation system that allows to represent and reason about knowledge represented in this way, based on a large and diverse class of logical primitives, including e.g. the coalitional behaviour of agents, quantitative uncertainty, counterfactual reasoning and default assumptions. This goes way beyond the current state of the art, where only logical primitives with a relational interpretation are supported by automated tools. Recent research has shown these new logical features can be accounted for in a uniform way by passing to a more general mathematical model, known as `coalgebraic semantics'. This richer framework does not only provide a uniform umbrella for a large number of reasoning principles, but also supports a rich mathematical theory that has by now matured to the extent which puts the development of automated tools within reach. The research challenge that this proposal addresses is the further development of these theoretical results as to bring them to bear on practical applications. As a concrete case study, we will use the Cool system to formalise quantitative models in Systems Biology.

- Development and prototypical implementation of decision procedures for global logical consequence for coalgebraic logics
- Development and prototypical implementation of decision procedures for hybrid coalgebraic logics
- Analysis of compositionality principles to account for both global logical consequence and hybrid extensions
- Implementation, optimisation and benchmarking of a coalgebraic description logic reasoning engine that allows for a modular combination of different reasoning principles
- Case Studies in Systems Biology

Email dirk@doc.ic.ac.uk for informal enquiries. Job adverts are available from the links below.

- for the Postdoctoral Position
- for the PhD Studentship

Dirk Pattinson | [check HTML] [check CSS] |