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

Sean McLaughlin; Clark Barrett; Yeting Ge

doi:10.1016/j.entcs.2005.12.005

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

Sean McLaughlin, Clark Barrett, Yeting Ge

Computer Science

Research output: Contribution to journal › Article › peer-review

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 language	English (US)
Pages (from-to)	43-51
Number of pages	9
Journal	Electronic Notes in Theoretical Computer Science
Volume	144
Issue number	2 SPEC. ISS.
DOIs	https://doi.org/10.1016/j.entcs.2005.12.005
State	Published - Jan 19 2006

Keywords

CVC
HOL
Proof checking
Theorem proving

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/j.entcs.2005.12.005

Cite this

@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",

note = "Funding Information: We{\textquoteright}d like to thank New York University, the University of Pittsburgh, Carnegie Mellon University, and the National Science Foundation (CCR-ITR-0325808) for their support of this work. We{\textquoteright}d also like to thank the referees for their helpful comments.",

year = "2006",

month = jan,

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

N1 - Funding Information: We’d like to thank New York University, the University of Pittsburgh, Carnegie Mellon University, and the National Science Foundation (CCR-ITR-0325808) for their support of this work. We’d also like to thank the referees for their helpful comments.

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

SN - 1571-0661

VL - 144

SP - 43

EP - 51

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2 SPEC. ISS.

ER -

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

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this