*Automated Deduction:* This also sometimes goes by the
name of Automated Reasoning or Automated Theoroem Proving. What
it means is the study of programs that prove theorems. The reason it is
sometimes called automated reasoning is because the computer is using
a form of reasoning, guided by the logical inference rules. Systems
that I work on are used to prove mathematical theorems, but that
is ony one use for them. One main interest in the field 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 exisiting algorithms so they
will be more efficient, and also to develop new algorithms based on new
techniques. In face, I am intersted in the development of efficient
algorithms in general.
| |