Combining Automated Theorem Provers and Computer Algebra Systems for Generating Formal Proofs of Complexity Bounds Extended Abstract

Over the past few years, the traditional separation between automated theorem provers and computer algebra systems has slowly been eroded as both sides venture into foreign ter-ritory. But despite recent progress, theorem provers still have difficulties with basic arithmetic while computer algebra sys-tem inherently produce “untrusted ” results that are not easily verified. We were able to combine successfully two such systems – NUPRL and MATHEMATICA – to build the Automated Com-plexity Analysis (ACA) system for analyzing the computa-tional complexity of higher-order functional programs. The ACA system automatically computes and proves correct an upper bound on the worst-case time complexity of a func-tional program synthesized by the NUPRL system. In this extended abstract, we briefly introduce our framework for reasoning informally about the computational complexity of higher-order functional programs and outline our approach to automation. We conclude with a description of employ-ing MATHEMATICA within the trusted NUPRL environment to construct a formal complexity proof