Kurt Gödel Research Center

2015 seminar talk: On Hestenes' geometric algebra: its formalization by the proof assistant and application to computational origami

Talk held by Tetsuo Ida (University of Tsukuba, Japan) at the KGRC seminar on 2015-10-01.

Abstract

We report the work of our on-going project on computational origami.
The first is the formalization of a Hestenes' geometric algebra (GA) by the proof assistant Isabelle/HOL. We use the notion of Classes of Isabelle/HOL to build up GA from more fundamental algebras. We restrict our algebra to 3D case since our immediate concern is the application of the 3D origami. The formalization of GA produces a set of algebraic equalities that involves operators of multiplication and addition of multi-vectors as well as inner and outer products. Those equalities are turned into Mathematica programs for practical computations of origami geometry.

The second is the integration of the obtained programs into our computation origami system Eos. Basing the geometric computation of Eos on GA requires significant changes of computing and proving engines of Eos. Our attempts so far are briefly explained.