Name
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.12.005 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
theorem proving,theorem provers,cvc lite,cooperating theorem provers,hol,proof checking,case study combining hol-light,case study,cvc,resulting proof,theorem prover | HOL,Theorem provers,Discrete mathematics,Proof checking,Computer science,Automated theorem proving | Journal |
Volume | Issue | ISSN |
144 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
26 | 1.24 | 8 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sean McLaughlin | 1 | 140 | 9.39 |
| Clark Barrett | 2 | 75 | 3.91 |
| Yeting Ge | 3 | 182 | 5.90 |