Risc Colloquium

We report two interim results 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 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.