Combining automated theorem provers and computer algebra systems for generating formal proofs of complexity bounds

摘要

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 territory. But despite recent progress, theorem provers still have difficulties with basic arithmetic while computer algebra system 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 Complexity Analysis (ACA) system for analyzing the computational 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 functional 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 employing MATHEMATICA within the trusted NUPRL environment to construct a formal complexity proof.