Professor Fitting
Professor Fitting is a logician. Formal logic is a subject that cuts across several disciplines, having applications to mathematics, computer science, artificial intelligence, philosophy, and linguistics. Professor Fitting has contributed to several of these areas. One of his recent books, co-authored with Raymond Smullyan, is on the foundations of set theory, and applies modal logic (see below) to establish basic results in the subject. But most of Professor Fitting's research is in areas other than mathematics.
One of the uses of formal logic in computer science is as a tool to provide meanings for computer languages, in a way that allows one to rigorously verify properties of programs. Professor Fitting has developed semantics for a family of programming languages, called logic programing languages. His work in this area has also been extended to apply to what is called non-monotonic reasoning, a fundamental subject in artificial intelligence. Non-monotonic reasoning is more like everyday reasoning than is reasoning in mathematics. Typically, we make plausible assumptions and act on them, withdrawing them if they are seen not to work (this is why it is called non-monotonic---assumptions come and go). Formalizing this kind of reasoning is an important goal of research.
Professor Fitting also works in the area of modal logics. These are logics that can be used to formalize reasoning involving qualified truth, such as: known to be true, believed to be true, true by the laws of physics, and so on. Currently Professor Fitting is extending his earlier work in this area to encompass more complex constructions, of the sort that occur in natural languages like English. This work applies both to artificial intelligence, and to philosophy, and Professor Fitting has published a recent book, with Richard Mendelsohn, on the philosophical aspects of this research.
Automation of reasoning is also an area in which Professor Fitting works, particularly the automation of reasoning involving the modal notions mentioned above. He has developed tableau proof systems which he, and others, have embodied in computer programs. Work in this area is currently a subject of considerable interest, especially in the Eurpean Computer Science community, and more and more efficient theorem-proving programs are under development worldwide, extending the work of Professor Fitting and that of many other researchers.