Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite |
| |
| Authors: | Sean McLaughlin Clark Barrett Yeting Ge |
| |
| Affiliation: | aDepartment of Computer Science, Carnegie Mellon University;bDepartment of Computer Science, New York University |
| |
| Abstract: | 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. |
| |
| Keywords: | HOL CVC theorem proving proof checking |
| 本文献已被 ScienceDirect 等数据库收录！ |
