Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite

This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.