I am interested in a wide range of different aspects of automated
reasoning. The following describes projects in my research group
with which I am involved.
Proof Planning: We have pioneered the use of proof
planning as a global strategy for guiding reasoning. Recent
work has focussed on the use of critics for patching failed
proof attempts. We are testing the generality and robustness of
proof planning by linking our clam proof planner to Mike
Gordon's hol theorem prover.
Inductive Proof: Most of our work has been on guiding
proofs by mathematical induction using proof plans. For
instance, we are investigating heuristics for selecting induction
rules. A lot of our current effort is focussed on extending
heuristic techniques originally devised for first-order logic to
higher-order.
Rippling: A lot of our effort has focussed on the {\e
rippling method, which tries to reduce the difference between
induction conclusion and induction hypothesis. We have adapted
rippling to reasoning about conjunctions of relations as in logic
programs and some hardware verification proofs. We are also
looking at rippling in a higher-order context.
Formal Methods: We have applied this work to the
verification, synthesis and transformation of software and
hardware. Recent work has focussed on hardware
verification, functional program synthesis, verifying
concurrent systems using CCS and proving properties of lazy
lists using coinduction. We are just starting to look at VDM
proof obligations.
Program Editor: We are applying techniques of program
synthesis to the construction of an editor for ML programs, which
supports programming by analogy and guarantees
well-definedness and termination.
Other Mathematics: We have also looked at summing
series and limit theorems, especially at the role of
rippling in these proofs.
Cooperative Problem Solving: We are using proof planning
to provide a high-level language for improving interactive
theorem provers.
Informal Reasoning: We are investigating how
reasoning with diagrams can be automated, using the
constructive omega rule.
Concept Formation: We are automating the formation of
group theoretic concepts. The value of concepts is assessed on a
multi-dimensional scale according to their ability to classify
finite groups.
Configuration: We have applied proof planning to the
configuration of computer systems and air compressors.
Bridge: We have also applied proof planning to the game of
bridge, including declarer play, bidding, drawing
inferences and tutor systems. We recently had a project on Go.
Uncertainty: We have developed a logic for reasoning under
uncertainty called incidence calculus. Sets of possible
worlds are associated with formulae, instead of numbers. Upper
and lower numeric bounds can be calculated from these possible
worlds. This arrangement enables incidence calculus to reason
with dependent information, which is not possible with purely
numeric uncertainty logics.