Which of the following refers to the proving of mathematical theorems by a computer program?

A. Analytical theorem proving

B. Automated technology proving

C. Automated theorem processing

D. Automated theorem proving

E. None of the choices.

Explanation:

Automated theorem proving (ATP) is the proving of mathematical theorems by a computer program. Depending on the underlying logic, the problem of deciding the validity of a theorem varies from trivial to impossible. Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification.