Research in Progress

The goal of this group is to explore the use of domainspecific knowledge and natural deduction-based reasoning techniques to construct theorem provers that operate in nontrivial mathematical domains. Two new provers, by Larry IIines and Tie-Cheng Wang, are very much like expert systems, since the prover takes its direction by trying to satisfy "higher level" goals, based on knowledge about theorem proving. These are stand-alone provers, not man-machine systems, which are attacking some fairly difficult theorems in mathematics. In addition to this mainline work on mathematical theorem provers, two auxiliary efforts rely heavily on knowledge-based deduction. Michael Starbird is developing a knowledge-based expert system for an area of geometric topology, particularly for three dimensions.