For most of my professional life I have worked on first-order logic theorem proving. On the more fundamental side of things I developed calculi and implementations based on hyper tableau, first-order DPLL (Model Evolution) and Resolution. Many of them have been extended for equality reasoning and reasoning modulo built-in theories, some for non-monotonic reasoning and some for temporal-logic model checking.
I am always interested in practical applications of automated reasoning systems. Applications of the above systems include database schema reasoning, consistency-based diagnosis, software verification, business process analysis, and situational awareness.
More recently I have shifted my focus on stochastic planning and model checking based on Markov Decision Processes. My co-workers are Sylvie Thiebaux and Felipe Trevizan.
See my CSIRO home page for a brief CV.