10-04-2017, 08:23 PM
Automated Theorem Proving
AbstractAutomated theorem proving (ATP), currently the most well-developed subfield of automated reasoning (AR), 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.