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.
@InProceedings{delima_et_al:LIPIcs.ITP.2024.11, author = {de Lima, Thaynara Arielly and Galdino, Andr\'{e} Luiz and de Oliveira Ribeiro, Bruno Berto and Ayala-Rinc\'{o}n, Mauricio}, title = {{A Formalization of the General Theory of Quaternions}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.11}, URN = {urn:nbn:de:0030-drops-207398}, doi = {10.4230/LIPIcs.ITP.2024.11}, annote = {Keywords: Theory of quaternions, Hamilton’s quaternions, Algebraic formalizations, PVS} }
Feedback for Dagstuhl Publishing