An investigation into the goals of research in automatic theorem proving as related to mathematical reasoning

摘要

We argue that theorem provers based on domain dependent knowledge must be able to increase their domain dependent deductive knowledge if they are to serve as a component of a mathematical reasoning system. The reason for this is that if such systems are not extensible then they would not be able to assimilate and use new deductive knowledge produced by a mathematical reasoning system.