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. As an application, we formalize some basic parts of two recently developed mathematical theories, namely, slice regular functions and Pythagorean-Hodograph curves.
Formalizing basic quaternionic analysis / Andrea Gabrielli; Marco Maggesi. - STAMPA. - 10499:(2017), pp. 225-240. (Intervento presentato al convegno ITP 2017 - Interactive Theorem Proving 2017 tenutosi a Brasilia (Brasile) nel 26 - 29 settembre 2017) [10.1007/978-3-319-66107-0_15].
Formalizing basic quaternionic analysis
Andrea Gabrielli;Marco Maggesi
2017
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. As an application, we formalize some basic parts of two recently developed mathematical theories, namely, slice regular functions and Pythagorean-Hodograph curves.
| File | Dimensione | Formato | |
|---|---|---|---|
|
ITP2017_Quaternionic.pdf
Accesso chiuso
Descrizione: Versione pubblicata online dall'editore
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Tutti i diritti riservati
Dimensione
233.31 kB
Formato
Adobe PDF
|
233.31 kB | Adobe PDF | Richiedi una copia |
|
itp2017.pdf
accesso aperto
Descrizione: Author Accepted Manuscript (AAM)
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Open Access
Dimensione
441.89 kB
Formato
Adobe PDF
|
441.89 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
