| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 423328 | Electronic Notes in Theoretical Computer Science | 2006 | 9 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
