简介

Research is in mathematical logic, especially higher-order logic (type theory) and automated theorem proving. It is 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 on Unix (including Linux) platforms. 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.