Document Open Access Logo

A Formalization of the General Theory of Quaternions

Authors Thaynara Arielly de Lima , André Luiz Galdino , Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.11.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Thaynara Arielly de Lima
  • Universidade Federal de Goiás, Goiânia, Brazil
André Luiz Galdino
  • Universidade Federal de Catalão, Catalão, Brazil
Bruno Berto de Oliveira Ribeiro
  • Universidade de Brasília, Brasília D.F., Brazil
Mauricio Ayala-Rincón
  • Universidade de Brasília, Brasília D.F., Brazil

Funding

  • de Lima, Thaynara Arielly: Project supported by FAPEG 202310267000223.
  • Ayala-Rincón, Mauricio: Project supported by FAPDF DE 00193.00001175/21-11 and CNPq Universal 409003/21-2 grants. The author was partially funded by the CNPq grant 313290/21-0.

Cite AsGet BibTex

Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón. A Formalization of the General Theory of Quaternions. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.11

Abstract

This paper discusses the formalization of the theory of quaternions in the Prototype Verification System (PVS). The general approach in this mechanization relies on specifying quaternion structures using any arbitrary field as a parameter. The approach allows the inheritance of formalized properties on quaternions when the parameters of the general theory are instantiated with specific fields such as reals or rationals. The theory includes characterizing algebraic properties that lead to constructing quaternions as division rings. In particular, we illustrate how the general theory is applied to formalize Hamilton’s quaternions using the field of reals as a parameter, for which we also mechanized theorems that show the completeness of three-dimensional rotations, proving that Hamilton’s quaternions mimic any 3D rotation.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Symbolic and algebraic manipulation
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
Keywords
  • Theory of quaternions
  • Hamilton’s quaternions
  • Algebraic formalizations
  • PVS

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. PVS system. https://pvs.csl.sri.com/index.html. Accessed: 2024-05-27.
  2. Reynald Affeldt and Cyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 30-42. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018629.
  3. Howard Anton and Chris Rorres. Elementary Linear Algebra: Applications Version. John Wiley & Sons. Inc., 10th edition, 2010. Google Scholar
  4. Mauricio Ayala-Rincón, Thaynara Arielly de Lima, André Luiz Galdino, and Andréia Borges Avelar. Formalization of Algebraic Theorems in PVS (Invited Talk). In Proc. 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR, volume 94 of EPiC Series in Computing, pages 1-10, 2023. URL: https://doi.org/10.29007/7jbv.
  5. Keith Conrad. Quaternion algebras. Accessed in March 13, 2024. URL: https://kconrad.math.uconn.edu/blurbs/ringtheory/quaternionalg.pdf.
  6. Thaynara Arielly de Lima, Andréia Borges Avelar, André Luiz Galdino, and Mauricio Ayala-Rincón. Formalizing factorization on euclidean domains and abstract euclidean algorithms. CoRR, abs/2404.14920, 2024. In Proceedings 18th Logical and Semantic Frameworks with Applications LSFA 2023. URL: https://doi.org/10.48550/arXiv.2404.14920.
  7. Thaynara Arielly de Lima, André Luiz Galdino, Andréia Borges Avelar, and Mauricio Ayala-Rincón. Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and Maximal Ideals, Chinese Remainder Theorem. J. Autom. Reason., 65(8):1231-1263, 2021. URL: https://doi.org/10.1007/s10817-021-09593-0.
  8. Ben L. Di Vito. Manip User’s Guide, Version 1.3, 2012. URL: https://pvs.csl.sri.com/doc/manip-guide.pdf.
  9. Andrea Gabrielli and Marco Maggesi. Formalizing Basic Quaternionic Analysis. In Proceedings of the 8th International Conference on Interactive Theorem Proving, ITP, volume 10499 of Lecture Notes in Computer Science, pages 225-240. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_15.
  10. Gökmen Günaşti. Quaternions algebra, their applications in rotations and beyond quaternions. Technical report, Linnaeus University, Digitala Vetenskapliga Arkivet, 2012. Google Scholar
  11. William Rowan Hamilton. On quaternions, or on a new system of imaginaries in algebra. Philosophical Magazine, 25(3):489-495, 1844. URL: https://doi.org/10.1080/14786444408645047.
  12. Israel (Yitzchak) Nathan Herstein. Topics in Algebra. John Wiley and Sons, New York, Chichester, Brisbane, Toronto, Singapore, second edition, 1975. Google Scholar
  13. Angeliki Koutsoukou-Argyraki. Octonions. Arch. Formal Proofs, 2018. URL: https://www.isa-afp.org/entries/Octonions.html.
  14. David W. Lewis. Quaternion Algebras and the Algebraic Legacy of Hamilton’s Quaternions. Irish Math. Soc. Bulletin, 57:41-64, 2006. URL: https://doi.org/10.33232/bims.0057.41.64.
  15. Paolo Masci and Aaron Dutle. Proof Mate: An interactive proof helper for PVS (tool paper). In Proceedings of the 14th International Symposium NASA Formal Methods, NFM 2022, volume 13260 of Lecture Notes in Computer Science, pages 809-815. Springer International Publishing, 2022. URL: https://doi.org/10.1007/978-3-031-06773-0_44.
  16. The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  17. César Muñoz and Micaela Mayero. Real Automation in the Field. Technical Report Interim report, No 39, NASA/ICASE, 2001. Google Scholar
  18. Lawrence C. Paulson. Quaternions. Arch. Formal Proofs, 2018. URL: https://www.isa-afp.org/entries/Quaternions.html.
  19. Logah Perumal. Euler angles: conversion of arbitrary rotation sequences to specific rotation sequence. Comput. Animat. Virtual Worlds, 25(5-6):521-529, 2014. URL: https://doi.org/10.1002/CAV.1529.
  20. Douglas Sweetser. Doing Physics with Quaternions, 2005. Accessed in March 13, 2024. URL: https://theworld.com/~sweetser/quaternions/ps/book.pdf.
  21. Douglas Sweetser. Three Roads to Quaternion Gravity. In APS March Meeting Abstracts, volume 2019 of APS Meeting Abstracts, page T70.008, January 2019. Google Scholar
  22. John Voight. Quaternion Algebras, volume GTM 288 of Graduate Texts in Mathematics. Springer Cham, 2021. URL: https://doi.org/10.1007/978-3-030-56694-4.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact