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

Sean McLaughlin, Clark Barrett, Yeting Ge

Research output: Contribution to journalArticle

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.

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

Fingerprint

Theorem
Object

Keywords

  • CVC
  • HOL
  • Proof checking
  • Theorem proving

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Cooperating theorem provers : A case study combining HOL-light and CVC lite. / McLaughlin, Sean; Barrett, Clark; Ge, Yeting.

In: Electronic Notes in Theoretical Computer Science, Vol. 144, No. 2 SPEC. ISS., 19.01.2006, p. 43-51.

Research output: Contribution to journalArticle

McLaughlin, Sean ; Barrett, Clark ; Ge, Yeting. / Cooperating theorem provers : A case study combining HOL-light and CVC lite. In: Electronic Notes in Theoretical Computer Science. 2006 ; Vol. 144, No. 2 SPEC. ISS. pp. 43-51.
@article{1315bc71e0394b2f8d71cb81ee3cdcba,
title = "Cooperating theorem provers: A case study combining HOL-light and CVC lite",
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 = "CVC, HOL, Proof checking, Theorem proving",
author = "Sean McLaughlin and Clark Barrett and Yeting Ge",
year = "2006",
month = "1",
day = "19",
doi = "10.1016/j.entcs.2005.12.005",
language = "English (US)",
volume = "144",
pages = "43--51",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "2 SPEC. ISS.",

}

TY - JOUR

T1 - Cooperating theorem provers

T2 - A case study combining HOL-light and CVC lite

AU - McLaughlin, Sean

AU - Barrett, Clark

AU - Ge, Yeting

PY - 2006/1/19

Y1 - 2006/1/19

N2 - 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.

AB - 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.

KW - CVC

KW - HOL

KW - Proof checking

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=30344433723&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=30344433723&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2005.12.005

DO - 10.1016/j.entcs.2005.12.005

M3 - Article

AN - SCOPUS:30344433723

VL - 144

SP - 43

EP - 51

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 2 SPEC. ISS.

ER -