Proving Theorems of Type Theory Automatically with TPS

Abstract

Reasoning plays an important role in many activities which involve intelligence, and it may be anticipated that automated reasoning will play a significant role in many applications of artificial intelligence. The importance of developing methods of automating reasoning has been recognized since the inception of research on artificial intelligence. One fruitful approach to this problem is to use the language and methods of symbolic logic. Since a great variety of problems can be expressed in symbolic logic, progress in developing general purpose reasoning tools based on symbolic logic has the potential to contribute to progress in many realms of artificial intelligence. Work on automated deduction using symbolic logic has been progressing steadily, but in recent years such work has been presented primarily at conferences on automated