Reasoning about Concrete Instances of Real-valued Functions in HOL4 using ACL2

Abstract:
Taking advantage of the high expressiveness of Higher-order logic (HOL), interactive theorem proving is extensively used in reasoning about subtle mathematical properties of reals and complex numbers that are described in symbolic form. However, while analyzing real-world systems, it may be necessary to reason about these properties on actual concrete instances, which may not be feasible within the HOL proof assistants, such as HOL4. In contrast, the ACL2 proof assistant possesses an inherent ability to reason
automatically and efficiently about concrete instances of functions. In this paper, we propose a methodology that utilizes the existing HOL4/ACL2 link to port real-valued functions, defined in HOL, to ACL2 for evaluation on concrete instances as well as for further reasoning. For illustration, we present a reliability analysis of medical diagnostic system by first symbolically verifying the reliability expression in HOL4. Then, we use the HOL4/ACL2 link to port this reliability expression to ACL2 for evaluation as well as reasoning about its error bounds on concrete instances.

Proof Script: Download