Logic and Computation Group: Research
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.
