Interactive vs. automated proofs in computational origami

This talk focuses on two important and subtle aspects in the specification of geometrical modeling. These aspects concern the so-called non-degeneracy and incident conditions. Non-degeneracy ensures that the specification can preclude the possibility that the model in question does not collapse into a degenerate version of the original one. On the other hand, an incident condition specifies that a given point is not on a given line. While an incident condition is in many situations a natural property, it may be subtle in certain geometric modeling and may therefore lead to nondegeneracy conditions. In this talk, we explain the non-degeneracy and incident conditions in the Huzita´s origami fold systems[1] that consist of (originally six) seven fold operations. We re-state Huzita´s origami operations and prove their basic geometrical properties related to fold in Isabelle/HOL. We then formally (in Isabelle/HOL) show that some of these operations will collapse into other operations when degenerate and incident cases occur. The part of proofs, i.e. those that require algebraic simplification into solved form, are performed by Mathematica.