Cool: Coalgebras, Ontologies and Logic

The main theme that underlies this research project is automatedreasoning, an applied sub-discipline of mathematical logic. Logichas found applications in many areas of computer sciencesuch as the verification of digital circuits, reasoning aboutprograms and knowledge representation. One of the most fundamentalaspects in this context is to automatically decide whether aparticular formula is a logical consequence of a given set ofassumptions. The set of assumptions may describe complex relationsbetween diseases and their symptoms, and one possible reasoning taskwould be to confirm or reject a diagnosis based on observed symptomsand medical history.In this research project, we investigate applications ofmathematical logic in knowledge representation. One of the primechallenges in this area is to design logical formalisms that strikea balance between the two conflicting goals of expressiveness (theability to formally represent the application domain) andcomputational tractability. The family of modal logics, conceived ina broad way, combines both aspects and serves as the mathematicalfoundation of a large number of knowledge representation formalisms.The core ingredient of modal logic is the possibility to qualifylogical assertions to hold in a certain way. Depending on thecontext, we may for instance stipulate that assertion holds `alwaysin the future', `with a likelihood of at least 50%' or `normally'.Together with names for individual entities, this allows us toformulate assertions like `the likelihood of congestion on Queen'sRoad is greater than 30%', and complex knowledge bases arise bycombining different logical primitives. Automated reasoning thenallows us to mechanically verify e.g. the consistency of scientifichypotheses against an existing knowledge base. Our goal is to builda modular and practical knowledge representation system that allowsto represent and reason about knowledge represented in this way,based on a large and diverse class of logical primitives, includinge.g. the coalitional behaviour of agents, quantitative uncertainty,counterfactual reasoning and default assumptions. This goes waybeyond the current state of the art, where only logical primitiveswith a relational interpretation are supported by automated tools.Recent research has shown these new logical features can beaccounted for in a uniform way by passing to a more generalmathematical model, known as `coalgebraic semantics'. This richerframework does not only provide a uniform umbrella for a largenumber of reasoning principles, but also supports a richmathematical theory that has by now matured to the extent which putsthe development of automated tools within reach. The researchchallenge that this proposal addresses is the further development of thesetheoretical results as to bring them to bear on practical applications.As a concrete case study, we will use the Cool system to formalisequantitative models in Systems Biology.