Cooperating theorem provers: A case study combining HOL-light and CVC lite

Sean McLaughlin, Clark Barrett, Yeting Ge

Research output: Contribution to journalArticle


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.

Original languageEnglish (US)
Pages (from-to)43-51
Number of pages9
JournalElectronic Notes in Theoretical Computer Science
Issue number2 SPEC. ISS.
StatePublished - Jan 19 2006



  • CVC
  • HOL
  • Proof checking
  • Theorem proving

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this