DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.11

A Formalization of the General Theory of Quaternions

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

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@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}
}

Search Results

Documents authored by Galdino, André Luiz

A Formalization of the General Theory of Quaternions

Abstract

Cite as

Thanks for your feedback!

Could not send message