Otter - The CADE-13 competition incarnations
This article discusses the two incarnations of Otter entered in the CADE-13 Automated Theorem Proving System Competition. Also presented are some historical background, a summary of applications that have led to new results in mathematics and logic, and a general discussion of Otter.
otter competition automated theorem proving automated reasoning equational deduction paramodulation resolution