Applications of theorem-proving to problem-solving

In this section we discuss how theorem-proving methods are being tested for several applications in the Stanford Research Institute Artificial Intelligence Group's Automaton (robot). We emphasize that this section describes work that is now in progress, rather than work that is completed. These methods represent explorations in problem solving, rather than final decisions about how the robot is to do problem solving. An overview of the current status of the entire SRI robot project is provided by Nilsson. Coles has developed an English-to-logic translator that is part of the robot.