Top-down Automated Theorem Proving (Notes for Sir Timothy)

C. E. Larson, N. Van Cleemput

We describe a "top down" approach for automated theorem proving (ATP). Researchers might usefully investigate the forms of the theorems mathematicians use in practice, carefully ex…