This grant will support a symposium, November 15 and 16, l991 at the University of Texas at Austin, on the research areas of automatic theorem proving and artificial intelligence. The symposium will be held in honor of Woodrow Bledsoe, a leading figure in combining the resolution and equality approaches of traditional automated reasoning with the heuristic approaches of artificial intelligence to achieve high performance inference. The symposium will provide an opportunity to analyze recent programs in these areas and to further the interplay between them.
