Automated theorem proving: An overview

Automated Theorem Provers are computer programs written to prove, or help in proving, mathematical and non-mathematical theorems. Automated Theorem Proving (ATP) is a rapidly advancing field and contains many potential research areas. This paper is an overview of this important field. It starts by giving the needed mathematical background followed by an overview. The overview includes historical background, basic terminology and notations and a description of the major components of a typical theorem prover. The paper also outlines the current state of research in ATP and a brief description of some of the existing theorem provers.