Research goals

Reasoning about action in robots,
Logic Summer School

Anything that makes sense can be subjected to logical analysis.

In the past, logic has been applied mainly to subject matter that does not depart too radically from the sort of examples found in logic textbooks: static, precise, clearly defined, sanitised. Part of our aim is to take logic out of its "comfort zone", making it confront realistic data and theories. It is possible to deal rationally with vague descriptions, for example, and logic should allow for such reasoning. It should not give up in the face of inconsistency either, for reasoning is needed with theories that have been assembled from parts which conflict with each other. It should be robust enough to cope where the data are changing faster than long chains of inference can be made. Logic needs to be pushed to confront situations which are too complex and generally too messy for easy analysis.

In order to make a difference, logic must be implemented.

Our research into algorithms for logical deduction spans both classical and non-classical logics. It also includes propositional proof search and satisfiability testing, first order theorem proving, and higher order user-guided reasoning. Our implemented systems rank among the world's best, as attested by their performance in competitions over a number of years, but we are more interested in pioneering new concepts in automated reasoning than in squeezing more inferences per second out of the well-worn ones. We believe that the potential for mechanised reasoning is far greater than its role in current practice, and set ourselves to help lead the movement towards computer-assisted rationality.

Logic is not an island.

The Logic and Computation group actively seeks collaboration with researchers in other disciplines who may benefit from our skills or our tools. For example, in NICTA our heaviest contributions are to two very ambitious projects, L4 Verified and the G12 Constraint Programming Platform, both of which not only push the boundaries of applied logic but also involve collaboration between multiple research programs and cross the boundaries between laboratories. It should be normal that any computing research project has a logician on the team.