Formalization of geometric algebra in HOL Light

DOI10.1007/s10817-018-9498-9zbMath1468.68329OpenAlexW2902885544MaRDI QIDQ2323452

Qianying Zhang, Zhiping Shi, Liming Li, Yong-Dong Li, Yong Guan

Publication date: 2 September 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9498-9

zbMATH Keywords

geometric algebrametricsHOL Lightformalizationmultivectors

Mathematics Subject Classification ID

Clifford algebras, spinors (15A66) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Formalizing geometric algebra in Lean ⋮ Verified interactive computation of definite integrals

Uses Software

• ACL2
• BIGEBRA
• CLIFFORD
• Isabelle
• ML
• Mizar
• HOL
• HOL Light
• GABLE
• GitHub
• kepler98

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Clifford and Graßmann Hopf algebras via the BIGEBRA package for Maple
• Implementing geometric algebra products with binary trees
• New foundations for classical mechanics.
• Isabelle. A generic theorem prover
• An elementary construction of the geometric algebra
• Formalizing basic quaternionic analysis
• Gröbner bases in Clifford and Grassmann algebras
• The HOL Light theory of Euclidean space
• Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
• HOL Light: An Overview
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Design and Implementation of an Embedded Coprocessor with Native Support for 5D, Quadruple-Based Clifford Algebra
• Theorem Proving in Higher Order Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalization of geometric algebra in HOL Light