Welcome to the Logic & Computation group

The Logic & Computation group at CECS traces its history via the Automated Reasoning Group (1994-2008) of the RSISE all the way back to the ANU Logic Group (1970-1993) founded by Bob Meyer and Richard Sylvan. It's research falls under three headings:

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.