Automated Deduction: This also sometimes goes by the name of Automated Reasoning or Automated Theorem Proving. One main interest in the field is to use these systems to verify that some specification is met, particularly a hardware or software specification. This could be very useful to prevent bugs, like what happened with the Pentium chip. My main contribution to this field is to make modification to currently existing algorithms so they will be more efficient, and also to develop new algorithms based on new techniques. In fact, I am interested in the development of efficient algorithms in general.