Automated theorem proving

Automated theorem proving (ATP) is a subfield of automated reasoning and mathematical logic proving mathematical theorems using computer programs. Automated reasoning added to mathematical proving was a major boost for computer science development.

Automated theorem proving is used commercially, concentrating on integrated circuit design and verification. Advanced Micro Devices (AMD), Intel and other companies use automated theorem proving to verify complicated floating point units of modern microprocessors and other operations are correctly implemented on the processors. Microprocessors have been designed with extra scrutiny since the Pentium FDIV bug affected Pentium and Intel processors in 1994.