Ò»±¾µÀÎÞÂë

My work has been motivated by the desire to help develop tools which will enhance the abilities of humans to reason. I look forward to the eventual formalization of virtually all mathematical, scientific, and technical knowledge, and the development of automated reasoning tools and automated information systems which use automated reasoning to assist in storing, developing, refining, verifying, finding, and applying this knowledge. Logical research will provide intellectual foundations for these developments.

My research has focused on automated deduction and Church's type theory, which is a rich and expressive formulation of higher-order logic in which statements from many disciplines, particularly those involving mathematics, can readily be expressed. The research has been directed toward enabling computers to construct and check proofs of theorems of mathematics and other disciplines formalized in type theory or first-order logic and to assist humans engaged in these tasks.

Potential applications of automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason, and certain aspects of artificial intelligence.

The research is based on an approach to automated theorem proving involving expansion proofs and matings. Expansion proofs and matings for a theorem represent the essential combinatorial structure of various proofs of the theorem. They can be found by heuristic search, and natural deduction proofs can be constructed from them without further search. A computer implementation of these ideas called TPS (Theorem Proving System) handles theorems of type theory as well as theorems of first-order logic. The system can be used in automatic or interactive mode, and is available to interested parties. It runs in Common Lisp. A subsystem of TPS called ETPS (Educational Theorem Proving System) is used as an interactive aid in logic courses. Research topics include the mathematical theory of matings and expansion proofs, improvements in heuristics used in searching for proofs and constructing elegant proofs, methods of finding appropriate substitutions for higher-order variables, and related questions.