Combining Automated Theorem Provers and Computer Algebra Systems for Generating Formal Proofs of Complexity Bounds Extended Abstract
Ralph Benzinger · 2002
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.