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. This technique fundamentally expands the capabilities of HOL-Light while preserving soundness.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Sean McLaughlin, Clark Barrett, Yeting Ge
• Keywords: Case Study, CVC PROVE, Derived Rule, ENTCS 2006