Automated Theorem Proving
- Natural & Formal Sciences -
Mathematics & Logic Dictionary
Definition
Automated theorem proving (ATP) is the use of algorithms and heuristics by software to perform proof search and establish theorems without human intervention, producing proofs or refutations in formal logics.