Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2509.19854 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866918147168141312 |
|---|---|
| author | Linzi, Alessandro |
| author_facet | Linzi, Alessandro |
| contents | We present a complete formalization in Isabelle/HOL of the object part of an equivalence between L-mosaics and bounded join-semilattices, employing an AI-assisted methodology that integrates large language models as reasoning assistants throughout the proof development process. The equivalence was originally established by Cangiotti, Linzi, and Talotti in their study of hypercompositional structures related to orthomodular lattices and quantum logic. Our formalization rigorously verifies the main theoretical result and demonstrates the mutual inverse property of the transformations establishing this equivalence. The development showcases both the mathematical depth of multivalued algebraic operations and the potential for AI-enhanced interactive theorem proving in tackling complex formalization projects. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_19854 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL Linzi, Alessandro Logic in Computer Science Commutative Algebra 68V20, 06A12 We present a complete formalization in Isabelle/HOL of the object part of an equivalence between L-mosaics and bounded join-semilattices, employing an AI-assisted methodology that integrates large language models as reasoning assistants throughout the proof development process. The equivalence was originally established by Cangiotti, Linzi, and Talotti in their study of hypercompositional structures related to orthomodular lattices and quantum logic. Our formalization rigorously verifies the main theoretical result and demonstrates the mutual inverse property of the transformations establishing this equivalence. The development showcases both the mathematical depth of multivalued algebraic operations and the potential for AI-enhanced interactive theorem proving in tackling complex formalization projects. |
| title | L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL |
| topic | Logic in Computer Science Commutative Algebra 68V20, 06A12 |
| url | https://arxiv.org/abs/2509.19854 |