Welcome to Holide
Holide is a proof translator. It takes proofs in OpenTheory's Repo and translates them to Dedukti format for proof checking. The most recent version is Holide2 (for proofs articles in OpenTheory version 6).
News
For the first time, all the proofs in OpenTheory repository were verified (with OpenTheory, Holide2 and Dedukti).
Download
Evaluation
The following two tables shows the difference between Holide1 and Holide2. The first table shows the size of article files and the translation time. The second table shows the size of translated files (in Dedukti format) and the corresponding proof checking time.
| Package | Holide1 | Holide2 | ||
|---|---|---|---|---|
| File Size (KB) | Time (s) | File Size (KB) | Time (s) | |
| base | 1,436 | 19.35 | 1,194 | 19.42 |
| cl | 313 | 5.77 | 313 | 5.56 |
| empty | 0 | 0.20 | 0 | 0.00 |
| gfp | 136 | 1.42 | 112 | 1.35 |
| lazy-list | 1390 | 31.43 | 1,391 | 31.78 |
| modular | 45 | 1.13 | 37 | 0.37 |
| natural-bits | 162 | 1.43 | 132 | 1.39 |
| natural-divides | 193 | 2.10 | 157 | 1.94 |
| natural-fibonacci | 130 | 1.31 | 108 | 1.24 |
| natural-prime | 140 | 1.46 | 116 | 1.34 |
| parser | 240 | 3.22 | 204 | 3.15 |
| probability | 26 | 0.30 | 23 | 0.23 |
| stream | 75 | 0.75 | 63 | 0.73 |
| word10 | 86 | 0.76 | 71 | 0.62 |
| word12 | 88 | 0.79 | 72 | 0.75 |
| word16 | 131 | 1.60 | 107 | 0.77 |
| word5 | 77 | 0.70 | 64 | 1.56 |
| Overall | 4,668 | 73.73 | 4,377 | 72.21 |
| Package | Dedukti (articles by Holide 1) | Dedukti (articles by Holide 2) | ||
|---|---|---|---|---|
| File Size (KB) | Time (s) | File Size (KB) | Time (s) | |
| base | 4,681 | 10.63 | 4,440 | 9.74 |
| cl | 1,219 | 2.42 | 1,219 | 2.46 |
| empty | 0 | 0.00 | 0 | 0.00 |
| gfp | 400 | 0.73 | 375 | 0.65 |
| lazy-list | 5718 | 13.31 | 5,717 | 13.11 |
| modular | 120 | 0.19 | 111 | 0.17 |
| natural-bits | 452 | 0.74 | 419 | 0.68 |
| natural-divides | 599 | 1.11 | 566 | 0.99 |
| natural-fibonacci | 378 | 0.67 | 354 | 0.60 |
| natural-prime | 408 | 0.72 | 388 | 0.65 |
| parser | 802 | 1.87 | 776 | 1.69 |
| probability | 72 | 0.12 | 69 | 0.11 |
| stream | 221 | 0.41 | 211 | 0.38 |
| word10 | 234 | 0.38 | 216 | 0.29 |
| word12 | 239 | 0.40 | 220 | 0.35 |
| word16 | 396 | 0.80 | 364 | 0.36 |
| word5 | 207 | 0.33 | 192 | 0.72 |
| Overall | 16,146 | 34.83 | 15,637 | 32.95 |
This announced the completion of proof checking of all OpenTheory packages avaliable. The success of checking of all these packages also shows the reliability of OpenTheory as a platform for higher order proofs. Further more, this verified the correctness of upgrade of Holide. In addition, this work also provided evidence for the correctness of HOL Light kernel and proofs from a different perspective.