Formalizing Basic Quaternionic Analysis

Andrea Gabrielli, Marco Maggesi

Presented at ITP 2017 - Interactive Theorem Proving.

Abstract

We present a computer formalization of quaternions in the HOL Light theorem prover. We give an introduction to our library for potential users and we discuss some implementation choices.

How to cite

Gabrielli A., Maggesi M. (2017)
Formalizing Basic Quaternionic Analysis.
In: Ayala-Rincón M., Muñoz C. (eds) Interactive Theorem Proving. ITP 2017.
Lecture Notes in Computer Science, vol 10499. Springer, Cham.

Download

BibTeX Entry

@Inbook{Gabrielli_Maggesi_ITP2017,
  author =	 "Gabrielli, Andrea and Maggesi, Marco",
  editor =	 "Ayala-Rinc{\'o}n, Mauricio and Mu{\~{n}}oz,
                  C{\'e}sar A.",
  title =	 "Formalizing Basic Quaternionic Analysis",
  bookTitle =	 "Interactive Theorem Proving: 8th International
                  Conference, ITP 2017, Bras{\'i}lia, Brazil,
                  September 26--29, 2017, Proceedings",
  year =	 "2017",
  publisher =	 "Springer International Publishing",
  address =	 "Cham",
  pages =	 "225--240",
  abstract =	 "We present a computer formalization of quaternions
                  in the HOL Light theorem prover. We give an
                  introduction to our library for potential users and
                  we discuss some implementation choices.",
  isbn =	 "978-3-319-66107-0",
  doi =		 "10.1007/978-3-319-66107-0_15",
  url =		 "https://doi.org/10.1007/978-3-319-66107-0_15" }

Marco Maggesi - University of Florence
Last modified: Wed Sep 27 13:23:26 -03 2017