There is relatively little work on the use of set theory in AI. McCarthy (1980) exploited sets in his nonmonotonic reasoning method circumscription (cf. Note 15). A weak set theory has been proposed as a specification language called SETL by Schwartz et al. (1986). Allgayer (1990) proposed an approach to introduce ways to talk and reason about sets into term languages like KL-ONE, which are widely used in natural language processing. Set theory has also been the subject of research in automated theorem proving. Data on the use of inference rules in student-constructed proofs in axiomatic set theory is presented in (Suppes & Sheehan 1981). The computer programs that are used in the computer-aided set theory course of Suppes and Sheehan represent perhaps the largest production programs created thus far for instructional purposes. Brown (1978) gave a deductive system for elementary set theory which is based on truth-value preserving transformations. Quaife (1992) presented a new clausal version of NBG set theory, comparing it with the one given in (Boyer et al. 1986), and claimed that automated development of set theory could be improved. We will now mention some essential research efforts, by Perlis, Zadrozny, Mislove et al., and Barwise towards a possible commonsense set theory.