Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.08264 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912580460609536 |
|---|---|
| author | Brown, Chad E. Kaliszyk, Cezary Suda, Martin Urban, Josef |
| author_facet | Brown, Chad E. Kaliszyk, Cezary Suda, Martin Urban, Josef |
| contents | We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of two. Higher order automated theorem provers are particularly useful here, since the underlying framework of higher order set theory coincides with the classical extensional higher order logic of (most) higher order automated theorem provers, so no significant translation or encoding is required. Additionally, many subgoals are first order and so first order automated provers often suffice. We compare the performance of different provers on the subgoals generated from the development. We also discuss possibilities for proof reconstruction, i.e., obtaining formal proof terms when an automated theorem prover claims to have proven the subgoal. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_08264 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Hammering Higher Order Set Theory Brown, Chad E. Kaliszyk, Cezary Suda, Martin Urban, Josef Logic in Computer Science We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of two. Higher order automated theorem provers are particularly useful here, since the underlying framework of higher order set theory coincides with the classical extensional higher order logic of (most) higher order automated theorem provers, so no significant translation or encoding is required. Additionally, many subgoals are first order and so first order automated provers often suffice. We compare the performance of different provers on the subgoals generated from the development. We also discuss possibilities for proof reconstruction, i.e., obtaining formal proof terms when an automated theorem prover claims to have proven the subgoal. |
| title | Hammering Higher Order Set Theory |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.08264 |