Formalizing Pick's Theorem in Isabelle/HOL
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909504776437760 |
|---|---|
| author | Binder, Sage Kosaian, Katherine |
| author_facet | Binder, Sage Kosaian, Katherine |
| contents | We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem in HOL Light, but tailor our proof approach to avoid a primary challenge point in his formalization, which is proving that any polygon with more than three vertices can be split (in its interior) by a line between some two vertices. We detail the approach we use to avoid this step and reflect on the pros and cons of our eventual formalization strategy. We use the theorem prover Isabelle/HOL, and our formalization involves augmenting the existing geometry libraries in various foundational ways (e.g., by adding the definition of a polygon and formalizing some key properties thereof). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_01793 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formalizing Pick's Theorem in Isabelle/HOL Binder, Sage Kosaian, Katherine Logic in Computer Science 03B35, 68V15, 68V20 F.3.1 We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem in HOL Light, but tailor our proof approach to avoid a primary challenge point in his formalization, which is proving that any polygon with more than three vertices can be split (in its interior) by a line between some two vertices. We detail the approach we use to avoid this step and reflect on the pros and cons of our eventual formalization strategy. We use the theorem prover Isabelle/HOL, and our formalization involves augmenting the existing geometry libraries in various foundational ways (e.g., by adding the definition of a polygon and formalizing some key properties thereof). |
| title | Formalizing Pick's Theorem in Isabelle/HOL |
| topic | Logic in Computer Science 03B35, 68V15, 68V20 F.3.1 |
| url | https://arxiv.org/abs/2405.01793 |