Electronic computers are mostly used to automate clerical tasks, but it is well known that they can also be programmed to play chess, compose music, and prove mathematical theorems. Since logical, mathematical reasoning is one of the purer forms of human, intellectual thought, the automation of such reasoning by means of electronic computers is a basic and challenging scientific problem. This book is about how computers can be used to construct and check mathematical proofs. This use of computers relies on their symbolic and deductive capabilities and is radically different from their use as fast numerical calculators. The impact of computers as intellectual, rather than clerical, tools is likely to be quite profound. This book tries to demonstrate in a concrete way that the capabilities of computing machines in this regard are quite powerful. It describes proofs of some significant theorems of mathematical logic that were completely checked by means of a computer.