With the generous sponsorship of the U.S. National Science Foundation, I had the 
privilege of visiting the ICOT Research Center and participating in its research program 
for nine months during September-November 1990, March-May 1991, and November 
1991-February 1992. It was a wonderful personal and professional experience. The 
people at ICOT were unfailingly kind and friendly. I would especially like to thank 
the people I worked most closely with: Masayuki Fujita and Ryuzo Hasegawa. I had 
many interesting technical and personal discussions with them and saw in them, and 
their colleagues, the time, energy, interest, and intelligence they invested in their re-
search. Fujita and Hasegawa shared my love of theorem proving research. I would also 
like to thank Koichi Furukawa, whom I met before coming to ICOT, who stimulated 
my interest in visiting ICOT, and with whom I also had many technical and personal 
discussions while at ICOT. He and Dr. Fuchi created the excellent research climate at 
ICOT and fostered the work on theorem proving there. I would like to thank Kazuhide 
lwata for his friendship and help with the daily details of living in Tokyo, including 
arranging for an apartment. I had good personal and professional interactions with 
too many other people at ICOT to name here. 

I was briefed on the research activities of the various laboratories at ICOT and 
found much high quality research that was of interest to me: constraint logic program-
ming, knowledge representation, natural language processing, parallel software and 
hardware, and, of course, theorem proving. In the end, though I would have enjoyed 
working on any number of activities at ICOT, I concentrated on theorem proving, the 
area of strongest personal interest and an area where I thought I could contribute the 
most while also demanding the least time of ICOT researchers to educate me in what 
they were doing. 

On various occasions, I lectured on the Prolog Technology Theorem Prover (PTTP), 
cost-based abductive inference, equality theorem proving, theory resolution, upside-
down meta-interpretation of model elimination, and theorem proving in general. While 
at ICOT, I researched and wrote about upside-down meta-interpretation of model elim-
ination, a unit-resulting extension of PTTP, and function and relation matching rules 
for building in theories. I discussed ICOT's MGTP, the earliest versions of which had 
already been written. I discussed the value and importance of term indexing to improve 


					- 111 -