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.
This work has been supported by GNSAGA-INdAM and MIUR.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Reachable from the url https://bitbucket.org/maggesi/quaternions/.
- 2.
Spivak, in his book Calculus on manifolds [10, p. 65], notices that if f(u, v) is a function and \(u=g(x,y)\) and \(v=h(x,y)\), then the chain rule is often written
$$\begin{aligned} \frac{\partial f}{\partial x} = \frac{\partial f}{\partial u}\frac{\partial u}{\partial x} + \frac{\partial f}{\partial v}\frac{\partial v}{\partial x}, \end{aligned}$$where f denotes two different functions on the left- and right-hand of the equation.
- 3.
Commit on Apr 10, 2017, HOL Light GitHub repository.
References
Ciolli, G., Gentili, G., Maggesi, M.: A certified proof of the Cartan fixed point theorems. J. Automated Reason. 47(3), 319–336 (2011). https://doi.org/10.1007/s10817-010-9198-6
Farouki, R.T., Giannelli, C., Manni, C., Sestini, A.: Identification of spatial PH quintic hermite interpolants with near-optimal shape measures. Comput. Aided Geom. Des. 25(4), 274–297 (2008)
Farouki, R.: Pythagorean-Hodograph Curves: Algebra and Geometry Inseparable. Geometry and Computing. Springer, Heidelberg (2009)
Fuchs, L., Théry, L.: Implementing geometric algebra products with binary trees. Adv. Appl. Clifford Algebras 24(2), 589–611 (2014)
Gentili, G., Stoppato, C., Struppa, D.: Regular Functions of a Quaternionic Variable. Springer Monographs in Mathematics. Springer, Heidelberg (2013)
Gentili, G., Struppa, D.C.: A new approach to Cullen-regular functions of a quaternionic variable. Comptes Rendus Math. 342(10), 741–744 (2006)
Harrison, J.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114–129. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_8
Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol. 10, no. 23, pp. 151–165. University of Białystok (2007). http://mizar.org/trybulec65/
Ma, S., Shi, Z., Shao, Z., Guan, Y., Li, L., Li, Y.: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Adv. Appl. Clifford Algebras 26(4), 1305–1330 (2016)
Spivak, M.: Calculus on Manifolds: A Modern Approach to Classical Theorems of Advanced Calculus. Advanced Book Program. Avalon Publishing, New York (1965)
Sudbery, A.: Quaternionic analysis. Math. Proc. Cambridge Philos. Soc. 85(02), 199–225 (1979)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Gabrielli, A., Maggesi, M. (2017). Formalizing Basic Quaternionic Analysis. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-66107-0_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66106-3
Online ISBN: 978-3-319-66107-0
eBook Packages: Computer ScienceComputer Science (R0)