Logic and Computation Group

Logical theory

The group has foci on proof theory and algebra. A good deal of the work concerns non-classical systems including modal, temporal and substructural logics. Much of the motivation comes from the need for special-purpose logics for reasoning about complex systems or to treat features of realistic data such as vagueness or inconsistency.

Mechanised reasoning

In order to be used, reasoning techniques should be implemented. We study automatic deduction, whereby software searches autonomously for proofs. We also study interactive reasoning systems, in which a human reasoner directs the deduction. Finally, we work on constraint satisfaction, where what is sought is not a proof of what must hold but rather a model of what might.

Applications of logic

We aim at the logical analysis of systems. That includes software systems, of course, but also much more: physical systems with both discrete and continuous aspects, systems of rules, communication protocols and so forth. Logical analysis is a tool for making future systems efficient, reliable and provably correct.